From a80e88cf10087725f5d25240b8074e9bc72e2e9c Mon Sep 17 00:00:00 2001
From: Alan Liang <symb@olic.link>
Date: Wed, 28 Aug 2024 15:16:15 +0800
Subject: [PATCH 1/5] Generalize evaluation context handling in AL [1/3]: AL
 generation

---
 spectec/spec/wasm-3.0/4-runtime.watsup        |   5 +
 spectec/src/al/al_util.ml                     |  35 ++--
 spectec/src/al/ast.ml                         |  12 +-
 spectec/src/al/eq.ml                          |  14 +-
 spectec/src/al/free.ml                        |  12 +-
 spectec/src/al/print.ml                       |  49 +----
 spectec/src/al/valid.ml                       |  14 +-
 spectec/src/al/walk.ml                        |  29 +--
 spectec/src/backend-interpreter/ds.ml         |  17 +-
 .../src/backend-interpreter/interpreter.ml    |   6 +-
 spectec/src/dune                              |   8 +-
 spectec/src/exe-watsup/main.ml                |  34 ++--
 spectec/src/il2al/manual.ml                   |   7 +-
 spectec/src/il2al/translate.ml                | 186 +++++-------------
 spectec/src/il2al/transpile.ml                |  25 +--
 15 files changed, 143 insertions(+), 310 deletions(-)

diff --git a/spectec/spec/wasm-3.0/4-runtime.watsup b/spectec/spec/wasm-3.0/4-runtime.watsup
index a3b913f545..077e7f6ed6 100644
--- a/spectec/spec/wasm-3.0/4-runtime.watsup
+++ b/spectec/spec/wasm-3.0/4-runtime.watsup
@@ -155,3 +155,8 @@ syntax instr/admin hint(desc "administrative instruction") =
   | FRAME_ n `{frame} instr*    hint(show FRAME_%#% %%)
   | HANDLER_ n `{catch*} instr* hint(show HANDLER_%#% %%)
   | TRAP
+
+syntax evalctx hint(desc "evaluation context") =
+  | LABEL_ n `{instr*}   hint(show LABEL_%#%)
+  | FRAME_ n `{frame}    hint(show FRAME_%#%)
+  | HANDLER_ n `{catch*} hint(show HANDLER_%#%)
diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml
index 4073e9e693..fba1728e22 100644
--- a/spectec/src/al/al_util.ml
+++ b/spectec/src/al/al_util.ml
@@ -61,13 +61,8 @@ let invCallE ?(at = no) ~note (id, il, el) = InvCallE (id, il, el) |> mk_expr at
 let iterE ?(at = no) ~note (e, idl, it) = IterE (e, idl, it) |> mk_expr at note
 let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
 let listE ?(at = no) ~note el = ListE el |> mk_expr at note
-let arityE ?(at = no) ~note e = ArityE e |> mk_expr at note
-let frameE ?(at = no) ~note (e_opt, e) = FrameE (e_opt, e) |> mk_expr at note
-let labelE ?(at = no) ~note (e1, e2) = LabelE (e1, e2) |> mk_expr at note
 let getCurStateE ?(at = no) ~note () = GetCurStateE |> mk_expr at note
-let getCurFrameE ?(at = no) ~note () = GetCurFrameE |> mk_expr at note
-let getCurLabelE ?(at = no) ~note () = GetCurLabelE |> mk_expr at note
-let getCurContextE ?(at = no) ~note () = GetCurContextE |> mk_expr at note
+let getCurContextE ?(at = no) ~note e = GetCurContextE e |> mk_expr at note
 let contE ?(at = no) ~note e = ContE e |> mk_expr at note
 let chooseE ?(at = no) ~note e = ChooseE e |> mk_expr at note
 let isCaseOfE ?(at = no) ~note (e, a) = IsCaseOfE (e, a) |> mk_expr at note
@@ -76,8 +71,7 @@ let contextKindE ?(at = no) ~note a = ContextKindE a |> mk_expr at note
 let isDefinedE ?(at = no) ~note e = IsDefinedE e |> mk_expr at note
 let matchE ?(at = no) ~note (e1, e2) = MatchE (e1, e2) |> mk_expr at note
 let hasTypeE ?(at = no) ~note (e, ty) = HasTypeE (e, ty) |> mk_expr at note
-let topLabelE ?(at = no) ~note () = TopLabelE |> mk_expr at note
-let topFrameE ?(at = no) ~note () = TopFrameE |> mk_expr at note
+let topContextE ?(at = no) ~note (id) = TopContextE id |> mk_expr at note
 let topValueE ?(at = no) ~note e_opt = TopValueE e_opt |> mk_expr at note
 let topValuesE ?(at = no) ~note e = TopValuesE e |> mk_expr at note
 let subE ?(at = no) ~note (id, ty) = SubE (id, ty) |> mk_expr at note
@@ -178,6 +172,12 @@ let rec typ_to_var_name ty =
   | Il.Ast.TupT tys -> List.map typ_to_var_name (List.map snd tys) |> String.concat "_"
   | Il.Ast.IterT (t, _) -> typ_to_var_name t
 
+let context_names = [
+  "FRAME_";
+  "LABEL_";
+  "HANDLER_";
+]
+
 (* Destruct *)
 
 let unwrap_optv: value -> value option = function
@@ -238,16 +238,17 @@ let args_of_casev = function
   | CaseV (_, vl) -> vl
   | v -> fail_value "args_of_casev" v
 
-let arity_of_framev: value -> value = function
-  | FrameV (Some v, _) -> v
-  | v -> fail_value "arity_of_framev" v
 
-let unwrap_framev: value -> value = function
-  | FrameV (_, v) -> v
-  | v -> fail_value "unwrap_framev" v
+(* Mixop *)
+
+let atom_of_name name typ = El.Atom.Atom name $$ no_region % (El.Atom.info typ)
+let atom_of_atom' atom' typ = atom' $$ no_region % (El.Atom.info typ)
 
+let frame_atom = atom_of_name "FRAME_" "evalctx"
+let frameE ?(at = no) ~note (arity, e) =
+  let frame_mixop = [[frame_atom]; [atom_of_atom' El.Atom.LBrace "evalctx"]; [atom_of_atom' El.Atom.RBrace "evalctx"]] in
+  caseE (frame_mixop, [arity; e]) ~at:at ~note:note
 
-(* Mixop *)
 
 let get_atom op =
   match List.find_opt (fun al -> List.length al <> 0) op with
@@ -268,10 +269,8 @@ let boolT = Il.Ast.BoolT $ no_region
 let natT = Il.Ast.NumT Il.Ast.NatT $ no_region
 let topT = varT "TOP" []
 let valT = varT "val" []
-let callframeT = varT "callframe" []
 let frameT = varT "frame" []
-let labelT = varT "label" []
-let handlerT = varT "handler" []
 let stateT = varT "state" []
 let instrT = varT "instr" []
 let admininstrT = varT "admininstr" []
+let evalctxT = varT "evalctx" []
diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index 5f2b896da2..97f9e94700 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -34,8 +34,6 @@ and value =
   | CaseV of id * value list           (* constructor *)
   | OptV of value option               (* optional value *)
   | TupV of value list                 (* tuple of values *)
-  | FrameV of value option * value     (* TODO: desugar using CaseV? *)
-  | LabelV of value * value            (* TODO: desugar using CaseV? *)
 
 type extend_dir =                      (* direction of extension *)
   | Front                              (* extend from the front *)
@@ -99,13 +97,8 @@ and expr' =
   | IterE of expr * id list * iter                (* expr (`{` id* `}`)* *)
   | OptE of expr option                           (* expr?  *)
   | ListE of expr list                            (* `[` expr* `]` *)
-  | ArityE of expr                                (* "the arity of expr" *)
-  | FrameE of expr option * expr                  (* "the activation of expr (with arity expr)?" *)
-  | LabelE of expr * expr                         (* "the label whose arity is expr and whose continuation is expr" *)
   | GetCurStateE                                  (* "the current state" *)
-  | GetCurFrameE                                  (* "the current frame" *)
-  | GetCurLabelE                                  (* "the current lbael" *)
-  | GetCurContextE                                (* "the current context" *)
+  | GetCurContextE of atom option                 (* "the current context of certain (Some) or any (None) type" *)
   | ContE of expr                                 (* "the continuation of" expr *)
   | ChooseE of expr                               (* "an element of" expr *)
   (* Conditions *)
@@ -115,8 +108,7 @@ and expr' =
   | IsDefinedE of expr                            (* expr is defined *)
   | MatchE of expr * expr                         (* expr matches expr *)
   | HasTypeE of expr * typ                        (* the type of expr is ty *)
-  | TopFrameE                                     (* "a frame is now on the top of the stack" *)
-  | TopLabelE                                     (* "a label is now on the top of the stack" *)
+  | TopContextE of atom                           (* "a context of type atom is now on the top of the stack" *)
   (* Conditions used in assertions *)
   | TopValueE of expr option                      (* "a value (of type expr)? is now on the top of the stack" *)
   | TopValuesE of expr                            (* "at least expr number of values on the top of the stack" *)
diff --git a/spectec/src/al/eq.ml b/spectec/src/al/eq.ml
index a3a373b4ac..6bb512f3b4 100644
--- a/spectec/src/al/eq.ml
+++ b/spectec/src/al/eq.ml
@@ -32,15 +32,8 @@ let rec eq_expr e1 e2 =
     eq_expr e1 e2 && il1 = il2 && it1 = it2
   | OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
   | ListE el1, ListE el2 -> eq_exprs el1 el2
-  | ArityE e1, ArityE e2 -> eq_expr e1 e2
-  | FrameE (eo1, e1), FrameE (eo2, e2) ->
-    eq_expr_opt eo1 eo2 && eq_expr e1 e2
-  | LabelE (e11, e12), LabelE (e21, e22) ->
-    eq_expr e11 e21 && eq_expr e12 e22
-  | GetCurStateE, GetCurStateE
-  | GetCurFrameE, GetCurFrameE
-  | GetCurLabelE, GetCurLabelE
-  | GetCurContextE, GetCurContextE -> true
+  | GetCurStateE, GetCurStateE -> true
+  | GetCurContextE i1, GetCurContextE i2 -> Option.equal (=) i1 i2
   | ContE e1, ContE e2 -> eq_expr e1 e2
   | ChooseE e1, ChooseE e2 -> eq_expr e1 e2
   | IsCaseOfE (e1, a1), IsCaseOfE (e2, a2) -> eq_expr e1 e2 && El.Atom.eq a1 a2
@@ -49,8 +42,7 @@ let rec eq_expr e1 e2 =
   | IsDefinedE e1, IsDefinedE e2 -> eq_expr e1 e2
   | MatchE (e11, e12), MatchE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
-  | TopLabelE, TopLabelE
-  | TopFrameE, TopFrameE -> true
+  | TopContextE i1, TopContextE i2 -> i1 = i2
   | TopValueE eo1, TopValueE eo2 -> eq_expr_opt eo1 eo2
   | TopValuesE e1, TopValuesE e2 -> eq_expr e1 e2
   | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2
diff --git a/spectec/src/al/free.ml b/spectec/src/al/free.ml
index 46106b0ea0..515d0d3d28 100644
--- a/spectec/src/al/free.ml
+++ b/spectec/src/al/free.ml
@@ -16,24 +16,19 @@ let rec free_expr expr =
   | NumE _
   | BoolE _
   | GetCurStateE
-  | GetCurLabelE
-  | GetCurContextE
-  | GetCurFrameE
+  | GetCurContextE _
   | ContextKindE _
   | YetE _ -> IdSet.empty
   | VarE id
   | SubE (id, _) -> IdSet.singleton id
   | UnE (_, e)
   | LenE e
-  | ArityE e
   | ContE e
   | ChooseE e -> free_expr e
   | BinE (_, e1, e2)
   | CompE (e1, e2)
   | CatE (e1, e2)
-  | MemE (e1, e2)
-  | LabelE (e1, e2) -> free_expr e1 @ free_expr e2
-  | FrameE (e_opt, e) -> free_opt free_expr e_opt @ free_expr e
+  | MemE (e1, e2) -> free_expr e1 @ free_expr e2
   | CallE (_, al)
   | InvCallE (_, _, al) ->  free_list free_arg al
   | TupE el
@@ -46,8 +41,7 @@ let rec free_expr expr =
   | OptE e_opt -> free_opt free_expr e_opt
   | IterE (e, _, i) -> free_expr e @ free_iter i
   | MatchE (e1, e2) -> free_expr e1 @ free_expr e2
-  | TopLabelE
-  | TopFrameE
+  | TopContextE _
   | TopValueE None -> IdSet.empty
   | IsDefinedE e
   | IsCaseOfE (e, _)
diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml
index e1499c1abf..42a4133176 100644
--- a/spectec/src/al/print.ml
+++ b/spectec/src/al/print.ml
@@ -58,10 +58,6 @@ let rec string_of_record r =
 
 and string_of_value =
   function
-  | LabelV (v1, v2) ->
-    sprintf "Label_%s %s" (string_of_value v1) (string_of_value v2)
-  | FrameV (None, v2) -> sprintf "(Frame %s)" (string_of_value v2)
-  | FrameV (Some v1, v2) -> sprintf "(Frame %s %s)" (string_of_value v1) (string_of_value v2)
   | ListV lv -> "[" ^ string_of_values ", " (Array.to_list !lv) ^ "]"
   | NumV n -> "0x" ^ Z.format "%X" n
   | BoolV b -> string_of_bool b
@@ -151,16 +147,9 @@ and string_of_expr expr =
   | MemE (e1, e2) ->
     sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
-  | ArityE e -> sprintf "arity(%s)" (string_of_expr e)
   | GetCurStateE -> "current_state()"
-  | GetCurLabelE -> "current_label()"
-  | GetCurFrameE -> "current_frame()"
-  | GetCurContextE -> "current_context()"
-  | FrameE (None, e2) ->
-    sprintf "callframe(%s)" (string_of_expr e2)
-  | FrameE (Some e1, e2) ->
-    sprintf "callframe(%s, %s)" (string_of_expr e1)
-      (string_of_expr e2)
+  | GetCurContextE None -> "current_context()"
+  | GetCurContextE (Some a) -> sprintf "current_context(%s)" (string_of_atom a)
   | ListE el -> "[" ^ string_of_exprs ", " el ^ "]"
   | AccE (e, p) -> sprintf "%s%s" (string_of_expr e) (string_of_path p)
   | ExtE (e1, ps, e2, dir) -> (
@@ -172,8 +161,6 @@ and string_of_expr expr =
   | StrE r -> string_of_record_expr r
   | ContE e -> sprintf "cont(%s)" (string_of_expr e)
   | ChooseE e -> sprintf "choose(%s)" (string_of_expr e)
-  | LabelE (e1, e2) ->
-    sprintf "label(%s, %s)" (string_of_expr e1) (string_of_expr e2)
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
@@ -184,6 +171,9 @@ and string_of_expr expr =
     let op' = List.map (fun al -> String.concat "" (List.map string_of_atom al)) op in
     (match op' with
     | [] -> "()"
+    | _::tl when List.length tl != List.length el ->
+      let res = String.concat ", " (List.map string_of_expr el) in
+      "(Invalid CaseE: " ^ (string_of_mixop op) ^ " (" ^ res ^ "))"
     | hd::tl ->
       let res =
         List.fold_left2 (
@@ -201,10 +191,7 @@ and string_of_expr expr =
   | IsCaseOfE (e, a) -> sprintf "case(%s) == %s" (string_of_expr e) (string_of_atom a)
   | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "valid(%s)" (string_of_expr e)
-  | TopLabelE -> "top_label()"
-    (* TODO: "type(top()) == label"*)
-  | TopFrameE -> "top_frame()"
-    (* TODO: "type(top()) == frame"*)
+  | TopContextE a -> sprintf "top_context(%s)" (string_of_atom a)
   | TopValueE (Some e) -> sprintf "top_value(%s)" (string_of_expr e)
   | TopValueE None -> "top_value()"
   | TopValuesE e -> sprintf "top_values(%s)" (string_of_expr e)
@@ -255,12 +242,8 @@ let enter_block f instrs =
 (* Prefix for stack push/pop operations *)
 let string_of_stack_prefix expr =
   match expr.it with
-  | GetCurContextE
-  | GetCurFrameE
-  | GetCurLabelE
+  | GetCurContextE _
   | ContE _
-  | LabelE _
-  | FrameE _
   | VarE ("F" | "L") -> ""
   | IterE _ -> ""
   | _ -> ""
@@ -389,8 +372,6 @@ let structured_string_of_ids ids =
 (* Values *)
 
 let rec structured_string_of_value = function
-  | LabelV (v1, v2) -> "LabelV (" ^ structured_string_of_value v1 ^ "," ^ structured_string_of_value v2 ^ ")"
-  | FrameV _ -> "FrameV (TODO)"
   | ListV lv -> "ListV" ^ "[" ^ string_of_values ", " (Array.to_list !lv) ^ "]"
   | BoolV b -> "BoolV (" ^ string_of_bool b ^ ")"
   | NumV n -> "NumV (" ^ Z.to_string n ^ ")"
@@ -465,12 +446,9 @@ and structured_string_of_expr expr =
     ^ structured_string_of_expr e2
     ^ ")"
   | LenE e -> "LenE (" ^ structured_string_of_expr e ^ ")"
-  | ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")"
   | GetCurStateE -> "GetCurStateE"
-  | GetCurLabelE -> "GetCurLabelE"
-  | GetCurFrameE -> "GetCurFrameE"
-  | GetCurContextE -> "GetCurContextE"
-  | FrameE _ -> "FrameE TODO"
+  | GetCurContextE None -> "GetCurContextE"
+  | GetCurContextE (Some a) -> sprintf "GetCurContextE (%s)" (string_of_atom a)
   | ListE el -> "ListE ([" ^ structured_string_of_exprs el ^ "])"
   | AccE (e, p) ->
     "AccE ("
@@ -499,12 +477,6 @@ and structured_string_of_expr expr =
   | StrE r -> "StrE (" ^ structured_string_of_record_expr r ^ ")"
   | ContE e1 -> "ContE (" ^ structured_string_of_expr e1 ^ ")"
   | ChooseE e1 -> "ChooseE (" ^ structured_string_of_expr e1 ^ ")"
-  | LabelE (e1, e2) ->
-    "LabelE ("
-    ^ structured_string_of_expr e1
-    ^ ", "
-    ^ structured_string_of_expr e2
-    ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
   | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
   | IterE (e, ids, iter) ->
@@ -526,8 +498,7 @@ and structured_string_of_expr expr =
   | HasTypeE (e, t) ->
     sprintf "HasTypeE (%s, %s)" (structured_string_of_expr e) (string_of_typ t)
   | IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
-  | TopLabelE -> "TopLabelE"
-  | TopFrameE -> "TopFrameE"
+  | TopContextE a -> "TopContextE (" ^ string_of_atom a ^ ")"
   | TopValueE None -> "TopValueE"
   | TopValueE (Some e) -> "TopValueE (" ^ structured_string_of_expr e ^ ")"
   | TopValuesE e -> "TopValuesE (" ^ structured_string_of_expr e ^ ")"
diff --git a/spectec/src/al/valid.ml b/spectec/src/al/valid.ml
index ce27621b59..8d70503232 100644
--- a/spectec/src/al/valid.ml
+++ b/spectec/src/al/valid.ml
@@ -456,19 +456,9 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
     l
     |> List.map note
     |> List.iter (check_match source elem_typ)
-  | ArityE expr1 ->
-    check_num source expr.note; check_context source expr1.note
-  | FrameE (expr_opt, expr1) ->
-    check_context source expr.note;
-    Option.iter (fun expr2 -> check_num source expr2.note) expr_opt;
-    check_match source expr1.note (varT "frame")
-  | LabelE (expr1, expr2) ->
-    check_context source expr.note;
-    check_num source expr1.note;
-    check_match source expr2.note (iterT (varT "instr") List)
-  | GetCurStateE | GetCurFrameE | GetCurLabelE | GetCurContextE ->
+  | GetCurStateE | GetCurContextE _ ->
     check_context source expr.note
-  | BoolE _  | IsCaseOfE _ | IsValidE _ | MatchE _ | HasTypeE _ | TopFrameE | TopLabelE ->
+  | BoolE _  | IsCaseOfE _ | IsValidE _ | MatchE _ | HasTypeE _ | TopContextE _ ->
     check_bool source expr.note
   | ContE expr1 ->
     check_match source expr.note (iterT (varT "instr") List);
diff --git a/spectec/src/al/walk.ml b/spectec/src/al/walk.ml
index 19cfb4cb25..17eb681d42 100644
--- a/spectec/src/al/walk.ml
+++ b/spectec/src/al/walk.ml
@@ -33,19 +33,17 @@ let walk_path (walker: unit_walker) (path: path) : unit =
 
 let walk_expr (walker: unit_walker) (expr: expr) : unit =
   match expr.it with
-  | VarE _ | SubE _ | NumE _ | BoolE _ | GetCurStateE | GetCurLabelE
-  | GetCurContextE | GetCurFrameE | YetE _ | TopLabelE | TopFrameE
+  | VarE _ | SubE _ | NumE _ | BoolE _ | GetCurStateE
+  | GetCurContextE _ | YetE _ | TopContextE _
   | TopValueE None | ContextKindE _ -> ()
 
-  | UnE (_, e) | LenE e | ArityE e | ContE e
+  | UnE (_, e) | LenE e | ContE e
   | IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
   | TopValueE (Some e) | TopValuesE e | ChooseE e -> walker.walk_expr walker e
-  
+
   | BinE (_, e1, e2) | CompE (e1, e2) | CatE (e1, e2) | MemE (e1, e2)
-  | LabelE (e1, e2) | MatchE (e1, e2) ->
+  | MatchE (e1, e2) ->
     walker.walk_expr walker e1; walker.walk_expr walker e2
-  | FrameE (e_opt, e) ->
-    Option.iter (walker.walk_expr walker) e_opt; walker.walk_expr walker e
   | CallE (_, al) | InvCallE (_, _, al) ->
     List.iter (walker.walk_arg walker) al
   | TupE el | ListE el | CaseE (_, el) ->
@@ -129,8 +127,8 @@ let walk_expr (walker: walker) (expr: expr) : expr =
   let walk_expr = walker.walk_expr walker in
   let it =
     match expr.it with
-    | NumE _ | BoolE _ | VarE _ | SubE _ | GetCurStateE | GetCurFrameE
-    | GetCurLabelE | GetCurContextE | ContextKindE _ | TopLabelE | TopFrameE | YetE _ -> expr.it
+    | NumE _ | BoolE _ | VarE _ | SubE _ | GetCurStateE
+    | GetCurContextE _ | ContextKindE _ | TopContextE _ | YetE _ -> expr.it
     | UnE (op, e) -> UnE (op, walk_expr e)
     | BinE (op, e1, e2) -> BinE (op, walk_expr e1, walk_expr e2)
     | CallE (id, al) -> CallE (id, List.map walk_arg al)
@@ -148,9 +146,6 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | CaseE (a, el) -> CaseE (a, List.map walk_expr el)
     | OptE e -> OptE (Option.map walk_expr e)
     | TupE el -> TupE (List.map walk_expr el)
-    | ArityE e -> ArityE (walk_expr e)
-    | FrameE (e1_opt, e2) -> FrameE (Option.map walk_expr e1_opt, walk_expr e2)
-    | LabelE (e1, e2) -> LabelE (walk_expr e1, walk_expr e2)
     | ContE e' -> ContE (walk_expr e')
     | ChooseE e' -> ChooseE (walk_expr e')
     | IterE (e, ids, iter) -> IterE (walk_expr e, ids, walk_iter iter)
@@ -248,9 +243,7 @@ let rec walk_expr f e =
       | NumE _
       | BoolE _
       | GetCurStateE
-      | GetCurFrameE
-      | GetCurLabelE
-      | GetCurContextE -> e.it
+      | GetCurContextE _ -> e.it
       | UnE (op, e') -> UnE (op, new_ e')
       | BinE (op, e1, e2) -> BinE (op, new_ e1, new_ e2)
       | CallE (id, al) -> CallE (id, List.map (walk_arg f) al)
@@ -268,9 +261,6 @@ let rec walk_expr f e =
       | CaseE (a, el) -> CaseE (a, List.map new_ el)
       | OptE e -> OptE (Option.map new_ e)
       | TupE el -> TupE (List.map new_ el)
-      | ArityE e' -> ArityE (new_ e')
-      | FrameE (e1_opt, e2) -> FrameE (Option.map new_ e1_opt, new_ e2)
-      | LabelE (e1, e2) -> LabelE (new_ e1, new_ e2)
       | ContE e' -> ContE (new_ e')
       | ChooseE e' -> ChooseE (new_ e')
       | VarE id -> VarE id
@@ -281,8 +271,7 @@ let rec walk_expr f e =
       | IsDefinedE e -> IsDefinedE (new_ e)
       | HasTypeE (e, t) -> HasTypeE(new_ e, t)
       | IsValidE e -> IsValidE (new_ e)
-      | TopLabelE -> e.it
-      | TopFrameE -> e.it
+      | TopContextE _ -> e.it
       | TopValueE (Some e) -> TopValueE (Some (new_ e))
       | TopValueE _ -> e.it
       | TopValuesE e -> TopValuesE (new_ e)
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
index f0a73188de..7098ef6848 100644
--- a/spectec/src/backend-interpreter/ds.ml
+++ b/spectec/src/backend-interpreter/ds.ml
@@ -274,21 +274,18 @@ module WasmContext = struct
     if List.length vs = 0 then Some ctx 
     else None
 
-  let get_current_frame () =
-    let match_frame = function
-      | FrameV _ -> true
+  let get_current_context typ =
+    let match_context = function
+      | CaseV (t, _) when t = typ -> true
       | _ -> false
-    in get_value_with_condition match_frame
+    in get_value_with_condition match_context
 
-  let get_current_label () =
-    let match_label = function
-      | LabelV _ -> true
-      | _ -> false
-    in get_value_with_condition match_label
+  let get_current_frame () =
+    get_current_context "FRAME_"
 
   let get_module_instance () =
     match get_current_frame () with
-    | FrameV (_, mm) -> mm
+    | CaseV (_, [_; mm]) -> mm
     | _ -> failwith "Invalid frame"
 
   (* Value stack *)
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 454cfca8e0..7157c4f238 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -582,16 +582,16 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
   *)
   | PushI e ->
     (match eval_expr env e with
-    | FrameV _ as v -> WasmContext.push_context (v, [], [])
+    | CaseV ("FRAME_", _) as v -> WasmContext.push_context (v, [], [])
     | ListV vs -> Array.iter WasmContext.push_value !vs
     | v -> WasmContext.push_value v
     );
     ctx
   | PopI e ->
     (match e.it with
-    | FrameE (_, inner_e) ->
+    | CaseE ([[{it = El.Atom.Atom "FRAME_"; _}]], [_; inner_e]) ->
       (match WasmContext.pop_context () with
-      | FrameV (_, inner_v), _, _ ->
+      | CaseV ("FRAME_", [_; inner_v]), _, _ ->
         let new_env = assign inner_e inner_v env in
         AlContext.set_env new_env ctx
       | v, _, _ -> failwith (sprintf "current context `%s` is not a frame" (string_of_value v))
diff --git a/spectec/src/dune b/spectec/src/dune
index 446b7d7b87..8165883fbe 100644
--- a/spectec/src/dune
+++ b/spectec/src/dune
@@ -7,10 +7,10 @@
     (re_export il)
     (re_export frontend)
     (re_export middlend)
-    (re_export backend_latex)
-    (re_export backend_prose)
-    (re_export backend_splice)
-    (re_export backend_interpreter)
+    ; (re_export backend_latex)
+    ; (re_export backend_prose)
+    ; (re_export backend_splice)
+    ; (re_export backend_interpreter)
     (re_export il2al)
   )
 )
diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml
index 68fb2fc07c..91884487af 100644
--- a/spectec/src/exe-watsup/main.ml
+++ b/spectec/src/exe-watsup/main.ml
@@ -10,7 +10,7 @@ type target =
  | Check
  | Latex
  | Prose of bool
- | Splice of Backend_splice.Config.t
+ (* | Splice of Backend_splice.Config.t *)
  | Interpreter of string list
 
 type pass =
@@ -115,7 +115,7 @@ let argspec = Arg.align
   "-d", Arg.Set dry, " Dry run (when -p) ";
   "-o", Arg.Unit (fun () -> file_kind := Output), " Output files";
   "-l", Arg.Set logging, " Log execution steps";
-  "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution";
+  (* "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution"; *)
   "-w", Arg.Unit (fun () -> warn_math := true; warn_prose := true),
     " Warn about unused or multiply used splices";
   "--warn-math", Arg.Set warn_math,
@@ -125,10 +125,10 @@ let argspec = Arg.align
 
   "--check", Arg.Unit (fun () -> target := Check), " Check only (default)";
   "--latex", Arg.Unit (fun () -> target := Latex), " Generate Latex";
-  "--splice-latex", Arg.Unit (fun () -> target := Splice Backend_splice.Config.latex),
+  (* "--splice-latex", Arg.Unit (fun () -> target := Splice Backend_splice.Config.latex),
     " Splice Sphinx";
   "--splice-sphinx", Arg.Unit (fun () -> target := Splice Backend_splice.Config.sphinx),
-    " Splice Sphinx";
+    " Splice Sphinx"; *)
   "--prose", Arg.Unit (fun () -> target := Prose true), " Generate prose";
   "--prose-rst", Arg.Unit (fun () -> target := Prose false), " Generate prose";
   "--interpreter", Arg.Rest_all (fun args -> target := Interpreter args),
@@ -146,7 +146,7 @@ let argspec = Arg.align
 ] @ List.map pass_argspec all_passes @ [
   "--all-passes", Arg.Unit (fun () -> List.iter enable_pass all_passes)," Run all passes";
 
-  "--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i), " The version of wasm, default to 3";
+  (* "--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i), " The version of wasm, default to 3"; *)
 
   "-help", Arg.Unit ignore, "";
   "--help", Arg.Unit ignore, "";
@@ -167,13 +167,13 @@ let () =
     if !print_el then
       Printf.printf "%s\n%!" (El.Print.string_of_script el);
     log "Elaboration...";
-    let il, elab_env = Frontend.Elab.elab el in
+    let il, _elab_env = Frontend.Elab.elab el in
     if !print_elab_il || !print_all_il then print_il il;
     log "IL Validation...";
     Il.Valid.valid il;
 
     (match !target with
-    | Prose _ | Splice _ | Interpreter _ ->
+    | Prose _ (* | Splice _ *) | Interpreter _ ->
       enable_pass Sideconditions;
     | _ when !print_al || !print_al_o <> "" ->
       enable_pass Sideconditions;
@@ -232,7 +232,7 @@ let () =
 
     | Latex ->
       log "Latex Generation...";
-      let config =
+      (* let config =
         Backend_latex.Config.{default with macros_for_ids = !latex_macros} in
       (match !odsts with
       | [] -> print_endline (Backend_latex.Gen.gen_string config el)
@@ -240,11 +240,11 @@ let () =
       | _ ->
         prerr_endline "too many output file names";
         exit 2
-      )
+      ) *)
 
-    | Prose as_plaintext ->
+    | Prose _as_plaintext ->
       log "Prose Generation...";
-      let config_latex = Backend_latex.Config.default in
+      (* let config_latex = Backend_latex.Config.default in
       let config_prose = Backend_prose.Config.{panic_on_error = false} in
       (match !odsts with
       | [] ->
@@ -263,9 +263,9 @@ let () =
       | _ ->
         prerr_endline "too many output file names";
         exit 2
-      )
+      ) *)
 
-    | Splice config ->
+    (* | Splice config ->
       if !in_place then
         odsts := !pdsts
       else
@@ -290,13 +290,13 @@ let () =
       let env = Backend_splice.Splice.(env config' !pdsts !odsts elab_env el prose) in
       List.iter2 (Backend_splice.Splice.splice_file ~dry:!dry env) !pdsts !odsts;
       if !warn_math then Backend_splice.Splice.warn_math env;
-      if !warn_prose then Backend_splice.Splice.warn_prose env;
+      if !warn_prose then Backend_splice.Splice.warn_prose env; *)
 
-    | Interpreter args ->
+    | Interpreter _args ->
       log "Initializing interpreter...";
-      Backend_interpreter.Ds.init al;
+      (* Backend_interpreter.Ds.init al;
       log "Interpreting...";
-      Backend_interpreter.Runner.run args
+      Backend_interpreter.Runner.run args *)
     );
     log "Complete."
   with
diff --git a/spectec/src/il2al/manual.ml b/spectec/src/il2al/manual.ml
index a9c649fd20..81fca5ab89 100644
--- a/spectec/src/il2al/manual.ml
+++ b/spectec/src/il2al/manual.ml
@@ -5,7 +5,6 @@ open Al_util
 
 type config = expr * expr * instr list
 
-let atom_of_name name typ = El.Atom.Atom name $$ no_region % (El.Atom.info typ)
 let varT id args = Il.Ast.VarT (id $ no_region, args) $ no_region
 let listT ty = Il.Ast.IterT (ty, Il.Ast.List) $ no_region
 
@@ -42,7 +41,7 @@ let return_instrs_of_instantiate config =
   let ty'' = Il.Ast.TupT (List.map (fun t -> no_name, t) [store.note; ty']) $ no_region in
   [
     enterI (
-      frameE (Some (numE Z.zero ~note:natT), frame) ~note:callframeT,
+      frameE (numE Z.zero ~note:natT, frame) ~note:evalctxT,
       catE (instrs, (listE [caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT] ~note:ty)) ~note:ty,
       vals
     );
@@ -65,12 +64,10 @@ let return_instrs_of_invoke config =
   [
     letI (arity,  len_expr);
     enterI (
-      frameE (Some (arity), frame) ~note:callframeT,
+      frameE (arity, frame) ~note:evalctxT,
       catE (instrs, listE [caseE ([[atom_of_name "FRAME_" "admininstr"]], []) ~note:admininstrT] ~note:ty) ~note:ty,
       vals
     );
     popI (iterE (value, ["val"], ListN (arity, None)) ~note:ty');
     returnI (Some (iterE (value, ["val"], ListN (arity, None)) ~note:ty'))
   ]
-
-
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index 82e3d5a632..5490a6a005 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -74,12 +74,6 @@ let args_of_case e =
   | _ -> error e.at
     (sprintf "cannot get arguments of case expression `%s`" (Il.Print.string_of_exp e))
 
-let context_names = [
-  "FRAME_";
-  "LABEL_";
-  "HANDLER_";
-]
-
 let is_context exp =
   is_case exp &&
   match case_of_case exp with
@@ -346,14 +340,10 @@ and translate_path path =
 let insert_assert exp =
   let at = exp.at in
   match exp.it with
-  | Il.CaseE ([{it = Il.Atom "FRAME_"; _}]::_, _) ->
-    assertI (topFrameE () ~note:boolT) ~at:at
+  | Il.CaseE ([{it = Il.Atom id; _}]::_, _) when List.mem id context_names ->
+    assertI (topContextE (atom_of_name id "evalctx") ~note:boolT) ~at:at
   | Il.IterE (_, (Il.ListN (e, None), _)) ->
     assertI (topValuesE (translate_exp e) ~at:at ~note:boolT) ~at:at
-  | Il.CaseE ([{it = Il.Atom "LABEL_"; _}]::_, { it = Il.TupE [ _n; _instrs; _vals ]; _ }) ->
-    assertI (topLabelE () ~at:at ~note:boolT) ~at:at
-  | Il.CaseE ([{it = Il.Atom "HANDLER_"; _}]::_, _) ->
-    assertI (yetE "a handler is now on the top of the stack" ~at:at ~note:boolT) ~at:at
   | Il.CaseE ([{it = Il.Atom "CONST"; _}]::_, { it = Il.TupE (ty' :: _); _ }) ->
     assertI (topValueE (Some (translate_exp ty')) ~note:boolT) ~at:at
   | _ ->
@@ -369,10 +359,8 @@ let cond_of_pop_value e =
     | Some {it = Il.Atom "VCONST"; _} -> topValueE (Some t) ~note:bt
     | _ -> topValueE None ~note:bt
     )
-  | GetCurFrameE ->
-    topFrameE () ~at:at ~note:bt
-  | GetCurLabelE ->
-    topLabelE () ~at:at ~note:bt
+  | GetCurContextE (Some a) ->
+    topContextE a ~at:at ~note:bt
   (* TODO: Remove this when pops is done *)
   | IterE (_, _, ListN (e', _)) ->
     topValuesE e' ~at:at ~note:bt
@@ -398,6 +386,8 @@ let insert_pop' e =
       popsI { (translate_exp e) with note = valsT } (Some (es |> List.length |> Z.of_int |> numE)) ~at:e.at
     | Il.IterE (_, (Il.ListN (e', None), _)) ->
       popsI { (translate_exp e) with note = valsT } (Some (translate_exp e')) ~at:e.at
+    | Il.IterE (_, (Il.List, _)) ->
+      popAllI { (translate_exp e) with note = valsT } ~at:e.at
     | _ ->
       popsI { (translate_exp e) with note = valsT } None ~at:e.at
   in
@@ -466,97 +456,34 @@ let rec translate_rhs exp =
   | _ when is_wasm_instr exp -> [ executeI (translate_exp exp) ]
   | _ -> error_exp exp "expression on rhs of reduction"
 
+and translate_context_instrs e' =
+  let e'' = listE [e'] ~note:(listT e'.note) in function
+  | { it = Il.ListE [ctx]; _ } when is_context ctx ->
+    (e'', translate_context_rhs ctx)
+  | { it = Il.CatE (ve, ie); _ } ->
+    (catE (translate_exp ie, e'') ~note:ie.note, [pushI (translate_exp ve)])
+  | { it = Il.ListE [ve; ie]; _ } ->
+    (listE [translate_exp ie; e'] ~note:ie.note, [pushI (translate_exp ve)])
+  | instrs ->
+    (catE (translate_exp instrs, e'') ~note:instrs.note, [])
+
 and translate_context_rhs exp =
   let at = exp.at in
   let note = exp.note in
-  let notes = listT note in
 
   let case = case_of_case exp in
   let atom = case |> List.hd |> List.hd in
   let args = args_of_case exp in
-  let case' = case |> Lib.List.split_last |> fst in
-
-  match atom.it, args with
-  | Il.Atom "FRAME_", [exp1; exp2; exp3] ->
-    let e1 = translate_exp exp1 in (* arity *)
-    let e2 = translate_exp exp2 in (* frame *)
-    let e3 = translate_rhs exp3 in (* label *)
-
-    let eF = varE "F"             ~at:at ~note:callframeT in (* frame id *)
-    let ef = frameE (Some e1, e2) ~at:at ~note:callframeT in (* frame *)
+  let case', _ = Lib.List.split_last case in
+  let args, instrs = Lib.List.split_last args in
 
-    let e' = caseE ([[atom]], []) ~note:note in
-    [
-      letI (eF, ef) ~at:at;
-      enterI (eF, listE [e'] ~note:notes, e3) ~at:at;
-    ]
-  | Il.Atom "LABEL_", [exp1; exp2; exp3] ->
-    let e1 = translate_exp exp1 in (* arity *)
-    let e2 = translate_exp exp2 in (* cont *)
-    let e3 = translate_exp exp3 in (* instrs *)
-
-    let eL = varE "L"        ~at:at ~note:labelT in (* label id *)
-    let el = labelE (e1, e2) ~at:at ~note:labelT in (* label *)
-
-    let at' = exp3.at in
-    let note' = exp3.note in
-    let exp'' = listE ([caseE ([[atom]], []) ~note:note]) ~at:at' ~note:note' in
-    (match exp3.it with
-    | Il.CatE (ve, ie) ->
-      [
-        letI (eL, el) ~at:at;
-        enterI (eL, catE (translate_exp ie, exp'') ~note:note', [pushI (translate_exp ve)]) ~at:at';
-      ]
-    | _ ->
-      [
-        letI (eL, el) ~at:at;
-        enterI (eL, catE(e3, exp'') ~note:note', []) ~at:at';
-      ]
-    )
-  | Il.Atom "HANDLER_", [exp1; exp2; exp3] ->
-    (match exp3.it with
-    | ListE [ctxt] when is_context ctxt ->
-      (* TODO: This case is very similar to Frame. Perhaps it can be generalized? *)
-      let e1 = translate_exp exp1 in (* arity *)
-      let e2 = translate_exp exp2 in (* catch *)
-      let e3 = translate_rhs exp3 in (* label *)
-
-      let eH = varE "H"                ~at:at ~note:handlerT in (* handler id *)
-      let eh = caseE (case', [e1; e2]) ~at:at ~note:handlerT in (* handler *)
-
-      let e' = caseE ([[atom]], []) ~note:note in
-      [
-        letI (eH, eh) ~at:at;
-        enterI (eH, listE [e'] ~note:notes, e3) ~at:at;
-      ]
-    | _ ->
-      (* TODO: This case is very similar to Label. Perhaps it can be generalized? *)
-      let e1 = translate_exp exp1 in (* arity *)
-      let e2 = translate_exp exp2 in (* catch *)
-      let e3 = translate_exp exp3 in (* instrs *)
-
-      let eH = varE "H"                ~at:at ~note:handlerT in (* handler id *)
-      let eh = caseE (case', [e1; e2]) ~at:at ~note:handlerT in (* handler *)
-
-      let at' = exp3.at in
-      let note' = exp3.note in
-      let exp' = caseE ([[atom]], []) ~note:note in
-      let exp'' = listE ([exp']) ~at:at' ~note:note' in
-
-      (match exp3.it with
-      | Il.ListE [ve; ie] -> (* HARDCODE *)
-        [
-          letI (eH, eh) ~at:at;
-          enterI (eH, listE [translate_exp ie; exp'] ~note:note', [pushI (translate_exp ve)]) ~at:at';
-        ]
-      | _ ->
-        [
-          letI (eH, eh) ~at:at;
-          enterI (eH, catE(e3, exp'') ~note:note', []) ~at:at';
-        ]
-      )
-    )
-  | _ -> error at ("unrecognized context: " ^ (Il.Print.string_of_atom atom))
+  let args' = List.map translate_exp args in
+  let e' = caseE ([[atom]], []) ~at:instrs.at ~note:instrs.note in
+  let instrs', al = translate_context_instrs e' instrs in
+  let ectx = caseE (case', args') ~at:at ~note:note in
+  [
+    enterI (ectx, instrs', al) ~at:at;
+  ]
 
 
 (* Handle pattern matching *)
@@ -1086,59 +1013,36 @@ let translate_context_winstr winstr =
   if not (is_context winstr) then [] else
 
   let at = winstr.at in
-  let kind = case_of_case winstr |> List.hd |> List.hd in
+  let case = case_of_case winstr in
+  let kind = case |> List.hd |> List.hd in
   let args = args_of_case winstr in
-
-  match kind.it with
-  (* Frame *)
-  | Il.Atom "FRAME_" ->
-    (match args with
-    | [arity; name; inner_exp] ->
-      [
-        letI (translate_exp name, getCurFrameE () ~note:name.note) ~at:at;
-        letI (translate_exp arity, arityE (translate_exp name) ~note:arity.note) ~at:at;
-        insert_assert inner_exp;
-      ]
-      @ insert_pop' (inner_exp) @
-      [
-        insert_assert winstr;
-        exitI kind ~at:at
-      ]
-    | _ -> error_exp winstr "wrong argument of frame"
-    )
-  (* Label, Handler *)
-  | _ ->
-    (* ASSUMPTION: the last arg is the inner stack of this context *)
-    let vals = Lib.List.last args in
-    [
-      (* TODO: append Jump instr *)
-      popAllI ({ (translate_exp vals) with note=(listT valT)}) ~at:vals.at;
-      insert_assert winstr;
-      exitI kind ~at:at
-    ]
+  let args, vals = Lib.List.split_last args in
+  (* The last element of case is for instr*, which should not be present in the context record *)
+  let case, _ = Lib.List.split_last case in
+
+  let destruct = caseE (case, List.map translate_exp args) ~note:evalctxT ~at:at in
+  [
+    letI (destruct, getCurContextE (Some kind) ~note:evalctxT) ~at:at;
+    insert_assert vals;
+  ] @ insert_pop' vals @ [
+    insert_assert winstr;
+    exitI kind ~at:at;
+  ]
 
 let translate_context ctx =
   let at = ctx.at in
 
   match ctx.it with
-  | Il.CaseE ([{it = Il.Atom "LABEL_"; at=at'; _} as atom]::_, { it = Il.TupE [ n; instrs ]; _ }) ->
-    let label = VarE "L" $$ at' % labelT in
-    [
-      letI (label, getCurLabelE () ~note:labelT) ~at:at;
-      letI (translate_exp n, arityE label ~note:n.note) ~at:at;
-      letI (translate_exp instrs, contE label ~note:instrs.note) ~at:at;
-    ],
-    exitI atom ~at:at
-  | Il.CaseE ([{it = Il.Atom "FRAME_"; _} as atom]::_, { it = Il.TupE [ n; f ]; _ }) ->
-    let frame = translate_exp f in
+  | Il.CaseE ([{it = Il.Atom id; _} as atom]::_ as case, { it = Il.TupE args; _ }) when List.mem id context_names ->
+    let destruct = caseE (case, List.map translate_exp args) ~note:evalctxT ~at:at in
     [
-      letI (frame, getCurFrameE () ~note:frameT) ~at:at;
-      letI (translate_exp n, arityE frame ~note:n.note) ~at:at;
+      letI (destruct, getCurContextE (Some atom) ~note:evalctxT) ~at:at;
     ],
     exitI atom ~at:at
   | Il.CaseE ([atom]::_, _) ->
     [
-      letI (translate_exp ctx, getCurContextE () ~note:ctx.note) ~at:at;
+      yetI "this should not happen";
+      letI (translate_exp ctx, getCurContextE (None) ~note:ctx.note) ~at:at;
     ],
     exitI atom ~at:at
   | _ -> [ yetI "TODO: translate_context" ~at:at ], yetI "TODO: translate_context"
diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml
index d3c145ea3d..e92f392ede 100644
--- a/spectec/src/il2al/transpile.ml
+++ b/spectec/src/il2al/transpile.ml
@@ -827,7 +827,9 @@ let insert_frame_binding instrs =
   in
 
   match Walk.walk_instrs walk_config instrs with
-  | il when !found -> (letI (varE "f" ~note:frameT, getCurFrameE () ~note:frameT)) :: il
+  | il when !found ->
+      let frame = frameE (varE "_" ~note:natT, varE "f" ~note:frameT) ~note:evalctxT in
+      (letI (frame, getCurContextE (Some frame_atom) ~note:evalctxT)) :: il
   | _ -> instrs
 
 
@@ -877,7 +879,8 @@ let handle_framed_algo a instrs =
   in
   (* End of helpers *)
 
-  let instr_hd = letI (e_zf, { e_zf with it = GetCurFrameE }) ~at:e_zf.at in
+  let frame = frameE (varE "_" ~note:natT, e_zf) ~note:evalctxT ~at:e_zf.at in
+  let instr_hd = letI (frame, getCurContextE (Some frame_atom) ~note:evalctxT) in
   let instr_tl = walk_instrs { default_config with
     post_instr;
     pre_expr = frame_finder;
@@ -906,14 +909,15 @@ let handle_unframed_algo instrs =
       match !frame_arg with
       | Some { it = ExpA f; _ } ->
         let callframeT = Il.Ast.VarT ("callframe" $ no_region, []) $ no_region in
-        let frame = frameE (None, f) ~at:f.at ~note:callframeT in
+        let zeroE = numE Z.zero ~note:natT in
+        let frame = frameE (zeroE, f) ~at:f.at ~note:callframeT in
         let frame' =
           match instr.it with
           (* HARDCODE: the frame-passing-style *)
           | LetI ( { it = TupE [f'; _]; _ }, _) ->
-            frameE (None, f') ~at:f'.at ~note:callframeT
+            frameE (zeroE, f') ~at:f'.at ~note:callframeT
           | _ ->
-            frameE (None, varE "_f" ~note:f.note) ~note:callframeT
+            frameE (zeroE, varE "_f" ~note:f.note) ~note:callframeT
         in
         [
           pushI frame ~at:frame.at;
@@ -994,10 +998,8 @@ let ensure_return il =
 let remove_exit algo =
   let exit_to_pop instr =
     match instr.it with
-    | ExitI ({ it = Atom.Atom "FRAME_"; _ }) ->
-      popI (getCurFrameE () ~note:frameT) ~at:instr.at
-    | ExitI ({ it = Atom.Atom "LABEL_"; _ }) ->
-      popI (getCurLabelE () ~note:labelT) ~at:instr.at
+    | ExitI ({ it = Atom.Atom id; _ }) when List.mem id context_names ->
+      popI (getCurContextE (Some (atom_of_name id "evalctx")) ~note:evalctxT) ~at:instr.at
     | _ -> instr
   in
 
@@ -1014,7 +1016,8 @@ let remove_exit algo =
 let remove_enter algo =
   let enter_frame_to_push_then_pop instr =
     match instr.it with
-    | EnterI (
+    (* TODO: fix *)
+    (* | EnterI (
       ({ it = FrameE (Some e_arity, _); _ } as e_frame),
       { it = CatE (instrs, { it = ListE ([ { it = CaseE ([[{ it = Atom.Atom "FRAME_"; _ }]], []); _ } ]); _ }); _ },
       il) ->
@@ -1038,7 +1041,7 @@ let remove_enter algo =
       ({ it = FrameE (None, _); _ } as e_frame),
       { it = ListE ([ { it = CaseE ([[{ it = Atom.Atom "FRAME_"; _ }]], []); _ } ]); _ },
       il) ->
-        pushI e_frame ~at:instr.at :: il @ [ popI e_frame ~at:instr.at ]
+        pushI e_frame ~at:instr.at :: il @ [ popI e_frame ~at:instr.at ] *)
     | _ -> [ instr ]
   in
 

From cfe535fa42b14c475f41c9c8427dbbfe2ee0c67a Mon Sep 17 00:00:00 2001
From: Alan Liang <symb@olic.link>
Date: Wed, 28 Aug 2024 15:35:52 +0800
Subject: [PATCH 2/5] Generalize evaluation context handling in AL [2/3]:
 interpreter backend

---
 spectec/src/al/al_util.ml                     | 10 +++-
 spectec/src/al/ast.ml                         |  2 -
 spectec/src/al/eq.ml                          |  2 -
 spectec/src/al/free.ml                        |  2 -
 spectec/src/al/print.ml                       |  5 --
 spectec/src/al/valid.ml                       |  6 +--
 spectec/src/al/walk.ml                        |  9 ++--
 spectec/src/backend-interpreter/builtin.ml    |  2 +-
 spectec/src/backend-interpreter/ds.ml         |  5 +-
 spectec/src/backend-interpreter/ds.mli        |  3 +-
 .../src/backend-interpreter/interpreter.ml    | 50 ++-----------------
 spectec/src/backend-prose/print.ml            |  2 -
 spectec/src/backend-prose/render.ml           |  3 --
 spectec/src/dune                              |  2 +-
 spectec/src/exe-watsup/main.ml                | 10 ++--
 spectec/src/il2al/translate.ml                |  4 +-
 16 files changed, 28 insertions(+), 89 deletions(-)

diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml
index fba1728e22..f5dce03c18 100644
--- a/spectec/src/al/al_util.ml
+++ b/spectec/src/al/al_util.ml
@@ -63,7 +63,6 @@ let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
 let listE ?(at = no) ~note el = ListE el |> mk_expr at note
 let getCurStateE ?(at = no) ~note () = GetCurStateE |> mk_expr at note
 let getCurContextE ?(at = no) ~note e = GetCurContextE e |> mk_expr at note
-let contE ?(at = no) ~note e = ContE e |> mk_expr at note
 let chooseE ?(at = no) ~note e = ChooseE e |> mk_expr at note
 let isCaseOfE ?(at = no) ~note (e, a) = IsCaseOfE (e, a) |> mk_expr at note
 let isValidE ?(at = no) ~note e = IsValidE e |> mk_expr at note
@@ -71,7 +70,6 @@ let contextKindE ?(at = no) ~note a = ContextKindE a |> mk_expr at note
 let isDefinedE ?(at = no) ~note e = IsDefinedE e |> mk_expr at note
 let matchE ?(at = no) ~note (e1, e2) = MatchE (e1, e2) |> mk_expr at note
 let hasTypeE ?(at = no) ~note (e, ty) = HasTypeE (e, ty) |> mk_expr at note
-let topContextE ?(at = no) ~note (id) = TopContextE id |> mk_expr at note
 let topValueE ?(at = no) ~note e_opt = TopValueE e_opt |> mk_expr at note
 let topValuesE ?(at = no) ~note e = TopValuesE e |> mk_expr at note
 let subE ?(at = no) ~note (id, ty) = SubE (id, ty) |> mk_expr at note
@@ -238,6 +236,14 @@ let args_of_casev = function
   | CaseV (_, vl) -> vl
   | v -> fail_value "args_of_casev" v
 
+let arity_of_framev: value -> value = function
+  | CaseV ("FRAME_", [v; _]) -> v
+  | v -> fail_value "arity_of_framev" v
+
+let unwrap_framev: value -> value = function
+  | CaseV ("FRAME_", [_; v]) -> v
+  | v -> fail_value "unwrap_framev" v
+
 
 (* Mixop *)
 
diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index 97f9e94700..8a7149295a 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -99,7 +99,6 @@ and expr' =
   | ListE of expr list                            (* `[` expr* `]` *)
   | GetCurStateE                                  (* "the current state" *)
   | GetCurContextE of atom option                 (* "the current context of certain (Some) or any (None) type" *)
-  | ContE of expr                                 (* "the continuation of" expr *)
   | ChooseE of expr                               (* "an element of" expr *)
   (* Conditions *)
   | IsCaseOfE of expr * atom                      (* expr is of the case atom *)
@@ -108,7 +107,6 @@ and expr' =
   | IsDefinedE of expr                            (* expr is defined *)
   | MatchE of expr * expr                         (* expr matches expr *)
   | HasTypeE of expr * typ                        (* the type of expr is ty *)
-  | TopContextE of atom                           (* "a context of type atom is now on the top of the stack" *)
   (* Conditions used in assertions *)
   | TopValueE of expr option                      (* "a value (of type expr)? is now on the top of the stack" *)
   | TopValuesE of expr                            (* "at least expr number of values on the top of the stack" *)
diff --git a/spectec/src/al/eq.ml b/spectec/src/al/eq.ml
index 6bb512f3b4..23d2df79ef 100644
--- a/spectec/src/al/eq.ml
+++ b/spectec/src/al/eq.ml
@@ -34,7 +34,6 @@ let rec eq_expr e1 e2 =
   | ListE el1, ListE el2 -> eq_exprs el1 el2
   | GetCurStateE, GetCurStateE -> true
   | GetCurContextE i1, GetCurContextE i2 -> Option.equal (=) i1 i2
-  | ContE e1, ContE e2 -> eq_expr e1 e2
   | ChooseE e1, ChooseE e2 -> eq_expr e1 e2
   | IsCaseOfE (e1, a1), IsCaseOfE (e2, a2) -> eq_expr e1 e2 && El.Atom.eq a1 a2
   | IsValidE e1, IsValidE e2 -> eq_expr e1 e2
@@ -42,7 +41,6 @@ let rec eq_expr e1 e2 =
   | IsDefinedE e1, IsDefinedE e2 -> eq_expr e1 e2
   | MatchE (e11, e12), MatchE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
-  | TopContextE i1, TopContextE i2 -> i1 = i2
   | TopValueE eo1, TopValueE eo2 -> eq_expr_opt eo1 eo2
   | TopValuesE e1, TopValuesE e2 -> eq_expr e1 e2
   | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2
diff --git a/spectec/src/al/free.ml b/spectec/src/al/free.ml
index 515d0d3d28..f6be8b5ad7 100644
--- a/spectec/src/al/free.ml
+++ b/spectec/src/al/free.ml
@@ -23,7 +23,6 @@ let rec free_expr expr =
   | SubE (id, _) -> IdSet.singleton id
   | UnE (_, e)
   | LenE e
-  | ContE e
   | ChooseE e -> free_expr e
   | BinE (_, e1, e2)
   | CompE (e1, e2)
@@ -41,7 +40,6 @@ let rec free_expr expr =
   | OptE e_opt -> free_opt free_expr e_opt
   | IterE (e, _, i) -> free_expr e @ free_iter i
   | MatchE (e1, e2) -> free_expr e1 @ free_expr e2
-  | TopContextE _
   | TopValueE None -> IdSet.empty
   | IsDefinedE e
   | IsCaseOfE (e, _)
diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml
index 42a4133176..0f49da5f1a 100644
--- a/spectec/src/al/print.ml
+++ b/spectec/src/al/print.ml
@@ -159,7 +159,6 @@ and string_of_expr expr =
   | UpdE (e1, ps, e2) ->
     sprintf "update(%s%s, %s)" (string_of_expr e1) (string_of_paths ps) (string_of_expr e2)
   | StrE r -> string_of_record_expr r
-  | ContE e -> sprintf "cont(%s)" (string_of_expr e)
   | ChooseE e -> sprintf "choose(%s)" (string_of_expr e)
   | VarE id -> id
   | SubE (id, _) -> id
@@ -191,7 +190,6 @@ and string_of_expr expr =
   | IsCaseOfE (e, a) -> sprintf "case(%s) == %s" (string_of_expr e) (string_of_atom a)
   | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "valid(%s)" (string_of_expr e)
-  | TopContextE a -> sprintf "top_context(%s)" (string_of_atom a)
   | TopValueE (Some e) -> sprintf "top_value(%s)" (string_of_expr e)
   | TopValueE None -> "top_value()"
   | TopValuesE e -> sprintf "top_values(%s)" (string_of_expr e)
@@ -243,7 +241,6 @@ let enter_block f instrs =
 let string_of_stack_prefix expr =
   match expr.it with
   | GetCurContextE _
-  | ContE _
   | VarE ("F" | "L") -> ""
   | IterE _ -> ""
   | _ -> ""
@@ -475,7 +472,6 @@ and structured_string_of_expr expr =
     ^ structured_string_of_expr e2
     ^ ")"
   | StrE r -> "StrE (" ^ structured_string_of_record_expr r ^ ")"
-  | ContE e1 -> "ContE (" ^ structured_string_of_expr e1 ^ ")"
   | ChooseE e1 -> "ChooseE (" ^ structured_string_of_expr e1 ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
   | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
@@ -498,7 +494,6 @@ and structured_string_of_expr expr =
   | HasTypeE (e, t) ->
     sprintf "HasTypeE (%s, %s)" (structured_string_of_expr e) (string_of_typ t)
   | IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
-  | TopContextE a -> "TopContextE (" ^ string_of_atom a ^ ")"
   | TopValueE None -> "TopValueE"
   | TopValueE (Some e) -> "TopValueE (" ^ structured_string_of_expr e ^ ")"
   | TopValuesE e -> "TopValuesE (" ^ structured_string_of_expr e ^ ")"
diff --git a/spectec/src/al/valid.ml b/spectec/src/al/valid.ml
index 8d70503232..e58299021d 100644
--- a/spectec/src/al/valid.ml
+++ b/spectec/src/al/valid.ml
@@ -458,14 +458,10 @@ let valid_expr (walker: unit_walker) (expr: expr) : unit =
     |> List.iter (check_match source elem_typ)
   | GetCurStateE | GetCurContextE _ ->
     check_context source expr.note
-  | BoolE _  | IsCaseOfE _ | IsValidE _ | MatchE _ | HasTypeE _ | TopContextE _ ->
+  | BoolE _  | IsCaseOfE _ | IsValidE _ | MatchE _ | HasTypeE _ | ContextKindE _ ->
     check_bool source expr.note
-  | ContE expr1 ->
-    check_match source expr.note (iterT (varT "instr") List);
-    check_match source expr1.note (varT "label")
   | ChooseE expr1 ->
     check_list source expr1.note; check_match source expr1.note (iterT expr.note List)
-  | ContextKindE _ -> () (* TODO: Not used anymore *)
   | IsDefinedE expr1 ->
     check_opt source expr1.note; check_bool source expr.note
   | TopValueE expr_opt ->
diff --git a/spectec/src/al/walk.ml b/spectec/src/al/walk.ml
index 17eb681d42..8ba3498041 100644
--- a/spectec/src/al/walk.ml
+++ b/spectec/src/al/walk.ml
@@ -34,10 +34,10 @@ let walk_path (walker: unit_walker) (path: path) : unit =
 let walk_expr (walker: unit_walker) (expr: expr) : unit =
   match expr.it with
   | VarE _ | SubE _ | NumE _ | BoolE _ | GetCurStateE
-  | GetCurContextE _ | YetE _ | TopContextE _
+  | GetCurContextE _ | YetE _
   | TopValueE None | ContextKindE _ -> ()
 
-  | UnE (_, e) | LenE e | ContE e
+  | UnE (_, e) | LenE e
   | IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
   | TopValueE (Some e) | TopValuesE e | ChooseE e -> walker.walk_expr walker e
 
@@ -128,7 +128,7 @@ let walk_expr (walker: walker) (expr: expr) : expr =
   let it =
     match expr.it with
     | NumE _ | BoolE _ | VarE _ | SubE _ | GetCurStateE
-    | GetCurContextE _ | ContextKindE _ | TopContextE _ | YetE _ -> expr.it
+    | GetCurContextE _ | ContextKindE _ | YetE _ -> expr.it
     | UnE (op, e) -> UnE (op, walk_expr e)
     | BinE (op, e1, e2) -> BinE (op, walk_expr e1, walk_expr e2)
     | CallE (id, al) -> CallE (id, List.map walk_arg al)
@@ -146,7 +146,6 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | CaseE (a, el) -> CaseE (a, List.map walk_expr el)
     | OptE e -> OptE (Option.map walk_expr e)
     | TupE el -> TupE (List.map walk_expr el)
-    | ContE e' -> ContE (walk_expr e')
     | ChooseE e' -> ChooseE (walk_expr e')
     | IterE (e, ids, iter) -> IterE (walk_expr e, ids, walk_iter iter)
     | IsCaseOfE (e, a) -> IsCaseOfE (walk_expr e, a)
@@ -261,7 +260,6 @@ let rec walk_expr f e =
       | CaseE (a, el) -> CaseE (a, List.map new_ el)
       | OptE e -> OptE (Option.map new_ e)
       | TupE el -> TupE (List.map new_ el)
-      | ContE e' -> ContE (new_ e')
       | ChooseE e' -> ChooseE (new_ e')
       | VarE id -> VarE id
       | SubE (id, t) -> SubE (id, t)
@@ -271,7 +269,6 @@ let rec walk_expr f e =
       | IsDefinedE e -> IsDefinedE (new_ e)
       | HasTypeE (e, t) -> HasTypeE(new_ e, t)
       | IsValidE e -> IsValidE (new_ e)
-      | TopContextE _ -> e.it
       | TopValueE (Some e) -> TopValueE (Some (new_ e))
       | TopValueE _ -> e.it
       | TopValuesE e -> TopValuesE (new_ e)
diff --git a/spectec/src/backend-interpreter/builtin.ml b/spectec/src/backend-interpreter/builtin.ml
index d641ec3c6e..c606fbcddf 100644
--- a/spectec/src/backend-interpreter/builtin.ml
+++ b/spectec/src/backend-interpreter/builtin.ml
@@ -141,7 +141,7 @@ let is_builtin = function
 
 let call name =
   let local =
-    WasmContext.get_current_frame ()
+    WasmContext.get_current_context "FRAME_"
     |> unwrap_framev
     |> strv_access "LOCALS"
     |> listv_nth
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
index 7098ef6848..bcc09757ba 100644
--- a/spectec/src/backend-interpreter/ds.ml
+++ b/spectec/src/backend-interpreter/ds.ml
@@ -280,11 +280,8 @@ module WasmContext = struct
       | _ -> false
     in get_value_with_condition match_context
 
-  let get_current_frame () =
-    get_current_context "FRAME_"
-
   let get_module_instance () =
-    match get_current_frame () with
+    match get_current_context "FRAME_" with
     | CaseV (_, [_; mm]) -> mm
     | _ -> failwith "Invalid frame"
 
diff --git a/spectec/src/backend-interpreter/ds.mli b/spectec/src/backend-interpreter/ds.mli
index ecdba4a3ee..da6c4272cb 100644
--- a/spectec/src/backend-interpreter/ds.mli
+++ b/spectec/src/backend-interpreter/ds.mli
@@ -69,8 +69,7 @@ module WasmContext : sig
   val string_of_context_stack : unit -> string
 
   val get_top_context : unit -> value option
-  val get_current_frame : unit -> value
-  val get_current_label : unit -> value
+  val get_current_context : id -> value
   val get_module_instance : unit -> value
 
   val get_value_stack : unit -> value list
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 7157c4f238..98ae316814 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -96,7 +96,6 @@ and access_path env base path =
   | DotP str -> (
     let str = Print.string_of_atom str in
     match base with
-    | FrameV (_, StrV r) -> Record.find str r
     | StrV r -> Record.find str r
     | v ->
       fail_path path
@@ -120,7 +119,6 @@ and replace_path env base path v_new =
     let str = Print.string_of_atom str in
     let r =
       match base with
-      | FrameV (_, StrV r) -> r
       | StrV r -> r
       | v ->
         fail_path path
@@ -299,38 +297,12 @@ and eval_expr env expr =
   | OptE opt -> Option.map (eval_expr env) opt |> optV
   | TupE el -> List.map (eval_expr env) el |> tupV
   (* Context *)
-  | ArityE e ->
-    (match eval_expr env e with
-    | LabelV (v, _) -> v
-    | FrameV (Some v, _) -> v
-    | FrameV _ -> numV Z.zero
-    | _ -> fail_expr expr "inner expr is not a context" (* Due to AL validation, unreachable *))
-  | FrameE (e_opt, e) ->
-    let arity =
-      match Option.map (eval_expr env) e_opt with
-      | None | Some (NumV _) as arity -> arity
-      | _ -> fail_expr expr "wrong arity of frame"
-    in
-    let r =
-      match eval_expr env e with
-      | StrV _ as v -> v
-      | _ -> fail_expr expr "inner expr is not a frame"
-    in
-    FrameV (arity, r)
-  | GetCurFrameE -> WasmContext.get_current_frame ()
-  | LabelE (e1, e2) ->
-    let v1 = eval_expr env e1 in
-    let v2 = eval_expr env e2 in
-    LabelV (v1, v2)
-  | GetCurLabelE -> WasmContext.get_current_label ()
-  | GetCurContextE ->
+  | GetCurContextE None ->
     (match WasmContext.get_top_context () with
     | None -> fail_expr expr "cannot get the current context"
     | Some ctxt -> ctxt)
-  | ContE e ->
-    (match eval_expr env e with
-    | LabelV (_, vs) -> vs
-    | _ -> fail_expr expr "inner expr is not a label")
+  | GetCurContextE (Some { it = Atom a; _ }) when List.mem a context_names ->
+    WasmContext.get_current_context a
   | ChooseE e ->
     let a = eval_expr env e |> unwrap_listv_to_array in
     if Array.length a = 0 then
@@ -362,21 +334,9 @@ and eval_expr env expr =
     | [v], Opt -> Option.some v |> optV
     | l, _ -> listV_of_list l)
   (* condition *)
-  | TopFrameE ->
-    let ctx = WasmContext.get_top_context () in
-    (match ctx with
-    | Some (FrameV _) -> boolV true
-    | _ -> boolV false)
-  | TopLabelE ->
-    let ctx = WasmContext.get_top_context () in
-    (match ctx with
-    | Some (LabelV _) -> boolV true
-    | _ -> boolV false)
   | ContextKindE a ->
     let ctx = WasmContext.get_top_context () in
     (match a.it, ctx with
-    | Atom "FRAME_", Some (FrameV _) -> boolV true
-    | Atom "LABEL_", Some (LabelV _) -> boolV true
     | Atom case, Some (CaseV (case', _)) -> boolV (case = case')
     | _ -> boolV false)
   | IsDefinedE e ->
@@ -589,7 +549,7 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     ctx
   | PopI e ->
     (match e.it with
-    | CaseE ([[{it = El.Atom.Atom "FRAME_"; _}]], [_; inner_e]) ->
+    | CaseE ([{it = El.Atom.Atom "FRAME_"; _}] :: _, [_; inner_e]) ->
       (match WasmContext.pop_context () with
       | CaseV ("FRAME_", [_; inner_v]), _, _ ->
         let new_env = assign inner_e inner_v env in
@@ -702,7 +662,7 @@ and step_wasm (ctx: AlContext.t) : value -> AlContext.t = function
   (* TODO: Change ref.null semantics *)
   | CaseV ("REF.NULL", [ ht ]) when !version = 3 ->
     let mm =
-      WasmContext.get_current_frame ()
+      WasmContext.get_current_context "FRAME_"
       |> unwrap_framev
       |> strv_access "MODULE"
     in
diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml
index 66493126bc..84e1226acb 100644
--- a/spectec/src/backend-prose/print.ml
+++ b/spectec/src/backend-prose/print.ml
@@ -145,7 +145,6 @@ and string_of_expr expr =
   | UpdE (e1, ps, e2) ->
     sprintf "%s with %s replaced by %s" (string_of_expr e1) (string_of_paths ps) (string_of_expr e2)
   | StrE r -> string_of_record_expr r
-  | ContE e -> sprintf "the continuation of %s" (string_of_expr e)
   | ChooseE e -> sprintf "an element of %s" (string_of_expr e)
   | LabelE (e1, e2) ->
     sprintf "the label_%s{%s}" (string_of_expr e1) (string_of_expr e2)
@@ -263,7 +262,6 @@ let string_of_stack_prefix expr =
   | GetCurContextE
   | GetCurFrameE
   | GetCurLabelE
-  | ContE _
   | LabelE _
   | FrameE _
   | VarE ("F" | "L") -> ""
diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index 2eec2c3573..69ac982544 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -421,9 +421,6 @@ and render_expr' env expr =
     let se1 = render_expr env e1 in
     let se2 = render_expr env e2 in
     sprintf "the activation of %s with arity %s" se2 se1
-  | Al.Ast.ContE e ->
-    let se = render_expr env e in
-    sprintf "the continuation of %s" se
   | Al.Ast.ChooseE e ->
     let se = render_expr env e in
     sprintf "an element of %s" se
diff --git a/spectec/src/dune b/spectec/src/dune
index 8165883fbe..79f8a2e147 100644
--- a/spectec/src/dune
+++ b/spectec/src/dune
@@ -10,7 +10,7 @@
     ; (re_export backend_latex)
     ; (re_export backend_prose)
     ; (re_export backend_splice)
-    ; (re_export backend_interpreter)
+    (re_export backend_interpreter)
     (re_export il2al)
   )
 )
diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml
index 91884487af..2b63bc04e4 100644
--- a/spectec/src/exe-watsup/main.ml
+++ b/spectec/src/exe-watsup/main.ml
@@ -115,7 +115,7 @@ let argspec = Arg.align
   "-d", Arg.Set dry, " Dry run (when -p) ";
   "-o", Arg.Unit (fun () -> file_kind := Output), " Output files";
   "-l", Arg.Set logging, " Log execution steps";
-  (* "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution"; *)
+  "-ll", Arg.Set Backend_interpreter.Runner.logging, " Log interpreter execution";
   "-w", Arg.Unit (fun () -> warn_math := true; warn_prose := true),
     " Warn about unused or multiply used splices";
   "--warn-math", Arg.Set warn_math,
@@ -146,7 +146,7 @@ let argspec = Arg.align
 ] @ List.map pass_argspec all_passes @ [
   "--all-passes", Arg.Unit (fun () -> List.iter enable_pass all_passes)," Run all passes";
 
-  (* "--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i), " The version of wasm, default to 3"; *)
+  "--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i), " The version of wasm, default to 3";
 
   "-help", Arg.Unit ignore, "";
   "--help", Arg.Unit ignore, "";
@@ -292,11 +292,11 @@ let () =
       if !warn_math then Backend_splice.Splice.warn_math env;
       if !warn_prose then Backend_splice.Splice.warn_prose env; *)
 
-    | Interpreter _args ->
+    | Interpreter args ->
       log "Initializing interpreter...";
-      (* Backend_interpreter.Ds.init al;
+      Backend_interpreter.Ds.init al;
       log "Interpreting...";
-      Backend_interpreter.Runner.run args *)
+      Backend_interpreter.Runner.run args
     );
     log "Complete."
   with
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index 5490a6a005..ce03168384 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -341,7 +341,7 @@ let insert_assert exp =
   let at = exp.at in
   match exp.it with
   | Il.CaseE ([{it = Il.Atom id; _}]::_, _) when List.mem id context_names ->
-    assertI (topContextE (atom_of_name id "evalctx") ~note:boolT) ~at:at
+    assertI (contextKindE (atom_of_name id "evalctx") ~note:boolT) ~at:at
   | Il.IterE (_, (Il.ListN (e, None), _)) ->
     assertI (topValuesE (translate_exp e) ~at:at ~note:boolT) ~at:at
   | Il.CaseE ([{it = Il.Atom "CONST"; _}]::_, { it = Il.TupE (ty' :: _); _ }) ->
@@ -360,7 +360,7 @@ let cond_of_pop_value e =
     | _ -> topValueE None ~note:bt
     )
   | GetCurContextE (Some a) ->
-    topContextE a ~at:at ~note:bt
+    contextKindE a ~at:at ~note:bt
   (* TODO: Remove this when pops is done *)
   | IterE (_, _, ListN (e', _)) ->
     topValuesE e' ~at:at ~note:bt

From 5b0a9b55622780e76e7410e4222453daea6df752 Mon Sep 17 00:00:00 2001
From: Alan Liang <symb@olic.link>
Date: Wed, 28 Aug 2024 15:49:29 +0800
Subject: [PATCH 3/5] Generalize evaluation context handling in AL [3/3]:
 backends other than interpreter

---
 spectec/src/backend-prose/print.ml  | 23 ++++-----------------
 spectec/src/backend-prose/render.ml | 31 +++++------------------------
 spectec/src/dune                    |  6 +++---
 spectec/src/exe-watsup/main.ml      | 22 ++++++++++----------
 spectec/src/il2al/encode.ml         |  8 +-------
 spectec/src/il2al/transpile.ml      | 10 ++--------
 6 files changed, 26 insertions(+), 74 deletions(-)

diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml
index 84e1226acb..07505129c7 100644
--- a/spectec/src/backend-prose/print.ml
+++ b/spectec/src/backend-prose/print.ml
@@ -126,16 +126,9 @@ and string_of_expr expr =
   | MemE (e1, e2) ->
     sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
-  | ArityE e -> sprintf "the arity of %s" (string_of_expr e)
   | GetCurStateE -> "the current state"
-  | GetCurLabelE -> "the current label"
-  | GetCurFrameE -> "the current frame"
-  | GetCurContextE -> "the current context"
-  | FrameE (None, e2) ->
-    sprintf "the activation of %s" (string_of_expr e2)
-  | FrameE (Some e1, e2) ->
-    sprintf "the activation of %s with arity %s" (string_of_expr e2)
-      (string_of_expr e1)
+  | GetCurContextE None -> "the current context"
+  | GetCurContextE (Some a) -> sprintf "the current %s context" (string_of_atom a)
   | ListE el -> "[" ^ string_of_exprs ", " el ^ "]"
   | AccE (e, p) -> sprintf "%s%s" (string_of_expr e) (string_of_path p)
   | ExtE (e1, ps, e2, dir) -> (
@@ -146,8 +139,6 @@ and string_of_expr expr =
     sprintf "%s with %s replaced by %s" (string_of_expr e1) (string_of_paths ps) (string_of_expr e2)
   | StrE r -> string_of_record_expr r
   | ChooseE e -> sprintf "an element of %s" (string_of_expr e)
-  | LabelE (e1, e2) ->
-    sprintf "the label_%s{%s}" (string_of_expr e1) (string_of_expr e2)
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
@@ -175,8 +166,6 @@ and string_of_expr expr =
   | IsCaseOfE (e, a) -> sprintf "%s is of the case %s" (string_of_expr e) (string_of_atom a)
   | HasTypeE (e, t) -> sprintf "the type of %s is %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "%s is valid" (string_of_expr e)
-  | TopLabelE -> "a label is now on the top of the stack"
-  | TopFrameE -> "a frame is now on the top of the stack"
   | TopValueE (Some e) -> sprintf "a value of value type %s is on the top of the stack" (string_of_expr e)
   | TopValueE None -> "a value is on the top of the stack"
   | TopValuesE e -> sprintf "there are at least %s values on the top of the stack" (string_of_expr e)
@@ -259,13 +248,9 @@ let make_index depth =
 (* Prefix for stack push/pop operations *)
 let string_of_stack_prefix expr =
   match expr.it with
-  | GetCurContextE
-  | GetCurFrameE
-  | GetCurLabelE
-  | LabelE _
-  | FrameE _
+  | GetCurContextE _
   | VarE ("F" | "L") -> ""
-  | _ when Il.Eq.eq_typ expr.note Al.Al_util.handlerT -> "the handler "
+  | _ when Il.Eq.eq_typ expr.note Al.Al_util.evalctxT -> "the evaluation context "
   | IterE _ -> "the values "
   | _ -> "the value "
 
diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index 69ac982544..f863d2fea1 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -407,27 +407,13 @@ and render_expr' env expr =
     let loop = Al.Al_util.iterE (ids, [], iter) ~note:Al.Al_util.no_note in
     let sloop = render_expr env loop in
     sprintf "for all %s, %s" sloop se
-  | Al.Ast.ArityE e ->
-    let se = render_expr env e in
-    sprintf "the arity of %s" se
   | Al.Ast.GetCurStateE -> "the current state"
-  | Al.Ast.GetCurLabelE -> "the current label"
-  | Al.Ast.GetCurFrameE -> "the current frame"
-  | Al.Ast.GetCurContextE -> "the current context"
-  | Al.Ast.FrameE (None, e2) ->
-    let se2 = render_expr env e2 in
-    sprintf "the activation of %s" se2
-  | Al.Ast.FrameE (Some e1, e2) ->
-    let se1 = render_expr env e1 in
-    let se2 = render_expr env e2 in
-    sprintf "the activation of %s with arity %s" se2 se1
+  | Al.Ast.GetCurContextE None -> "the current context"
+  | Al.Ast.GetCurContextE (Some a) ->
+    sprintf "the current %s context" (render_atom env a)
   | Al.Ast.ChooseE e ->
     let se = render_expr env e in
     sprintf "an element of %s" se
-  | Al.Ast.LabelE (e1, e2) ->
-    let se1 = render_expr env e1 in
-    let se2 = render_expr env e2 in
-    sprintf "the label whose arity is %s and whose continuation is %s" se1 se2
   | Al.Ast.ContextKindE a ->
     let sa = render_atom env a in
     sprintf "the top of the stack is a %s" sa
@@ -444,8 +430,6 @@ and render_expr' env expr =
   | Al.Ast.IsValidE e ->
     let se = render_expr env e in
     sprintf "%s is valid" se
-  | Al.Ast.TopLabelE -> "a label is now on the top of the stack"
-  | Al.Ast.TopFrameE -> "a frame is now on the top of the stack"
   | Al.Ast.TopValueE (Some e) ->
     let se = render_expr env e in
     sprintf "a value of value type %s is on the top of the stack" se
@@ -551,14 +535,9 @@ and render_prose_instrs env depth instrs =
 (* Prefix for stack push/pop operations *)
 let render_stack_prefix expr =
   match expr.it with
-  | Al.Ast.GetCurContextE
-  | Al.Ast.GetCurFrameE
-  | Al.Ast.GetCurLabelE
-  | Al.Ast.ContE _
-  | Al.Ast.FrameE _
-  | Al.Ast.LabelE _
+  | Al.Ast.GetCurContextE _
   | Al.Ast.VarE ("F" | "L") -> ""
-  | _ when Il.Eq.eq_typ expr.note Al.Al_util.handlerT -> "the handler "
+  | _ when Il.Eq.eq_typ expr.note Al.Al_util.evalctxT -> "the evaluation context "
   | Al.Ast.IterE _ -> "the values "
   | _ -> "the value "
 
diff --git a/spectec/src/dune b/spectec/src/dune
index 79f8a2e147..446b7d7b87 100644
--- a/spectec/src/dune
+++ b/spectec/src/dune
@@ -7,9 +7,9 @@
     (re_export il)
     (re_export frontend)
     (re_export middlend)
-    ; (re_export backend_latex)
-    ; (re_export backend_prose)
-    ; (re_export backend_splice)
+    (re_export backend_latex)
+    (re_export backend_prose)
+    (re_export backend_splice)
     (re_export backend_interpreter)
     (re_export il2al)
   )
diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml
index 2b63bc04e4..3698ba1cb0 100644
--- a/spectec/src/exe-watsup/main.ml
+++ b/spectec/src/exe-watsup/main.ml
@@ -10,7 +10,7 @@ type target =
  | Check
  | Latex
  | Prose of bool
- (* | Splice of Backend_splice.Config.t *)
+ | Splice of Backend_splice.Config.t
  | Interpreter of string list
 
 type pass =
@@ -125,10 +125,10 @@ let argspec = Arg.align
 
   "--check", Arg.Unit (fun () -> target := Check), " Check only (default)";
   "--latex", Arg.Unit (fun () -> target := Latex), " Generate Latex";
-  (* "--splice-latex", Arg.Unit (fun () -> target := Splice Backend_splice.Config.latex),
+  "--splice-latex", Arg.Unit (fun () -> target := Splice Backend_splice.Config.latex),
     " Splice Sphinx";
   "--splice-sphinx", Arg.Unit (fun () -> target := Splice Backend_splice.Config.sphinx),
-    " Splice Sphinx"; *)
+    " Splice Sphinx";
   "--prose", Arg.Unit (fun () -> target := Prose true), " Generate prose";
   "--prose-rst", Arg.Unit (fun () -> target := Prose false), " Generate prose";
   "--interpreter", Arg.Rest_all (fun args -> target := Interpreter args),
@@ -167,7 +167,7 @@ let () =
     if !print_el then
       Printf.printf "%s\n%!" (El.Print.string_of_script el);
     log "Elaboration...";
-    let il, _elab_env = Frontend.Elab.elab el in
+    let il, elab_env = Frontend.Elab.elab el in
     if !print_elab_il || !print_all_il then print_il il;
     log "IL Validation...";
     Il.Valid.valid il;
@@ -232,7 +232,7 @@ let () =
 
     | Latex ->
       log "Latex Generation...";
-      (* let config =
+      let config =
         Backend_latex.Config.{default with macros_for_ids = !latex_macros} in
       (match !odsts with
       | [] -> print_endline (Backend_latex.Gen.gen_string config el)
@@ -240,11 +240,11 @@ let () =
       | _ ->
         prerr_endline "too many output file names";
         exit 2
-      ) *)
+      )
 
-    | Prose _as_plaintext ->
+    | Prose as_plaintext ->
       log "Prose Generation...";
-      (* let config_latex = Backend_latex.Config.default in
+      let config_latex = Backend_latex.Config.default in
       let config_prose = Backend_prose.Config.{panic_on_error = false} in
       (match !odsts with
       | [] ->
@@ -263,9 +263,9 @@ let () =
       | _ ->
         prerr_endline "too many output file names";
         exit 2
-      ) *)
+      )
 
-    (* | Splice config ->
+    | Splice config ->
       if !in_place then
         odsts := !pdsts
       else
@@ -290,7 +290,7 @@ let () =
       let env = Backend_splice.Splice.(env config' !pdsts !odsts elab_env el prose) in
       List.iter2 (Backend_splice.Splice.splice_file ~dry:!dry env) !pdsts !odsts;
       if !warn_math then Backend_splice.Splice.warn_math env;
-      if !warn_prose then Backend_splice.Splice.warn_prose env; *)
+      if !warn_prose then Backend_splice.Splice.warn_prose env;
 
     | Interpreter args ->
       log "Initializing interpreter...";
diff --git a/spectec/src/il2al/encode.ml b/spectec/src/il2al/encode.ml
index 4c21466d28..806e3a1edc 100644
--- a/spectec/src/il2al/encode.ml
+++ b/spectec/src/il2al/encode.ml
@@ -41,19 +41,13 @@ let args_of_case e =
   | CaseE (_, exp) -> [ exp ]
   | _ -> error e.at "cannot get arguments of case expression"
 
-let context_names = [
-  "FRAME_";
-  "LABEL_";
-  "HANDLER_";
-]
-
 let is_context e =
   is_case e &&
   match case_of_case e with
   | (atom :: _) :: _ ->
     (match it atom with
 
-  | Atom a -> List.mem a context_names
+  | Atom a -> List.mem a Al.Al_util.context_names
     | _ -> false)
   | _ -> false
 
diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml
index e92f392ede..7b9a2dbc4f 100644
--- a/spectec/src/il2al/transpile.ml
+++ b/spectec/src/il2al/transpile.ml
@@ -1016,9 +1016,8 @@ let remove_exit algo =
 let remove_enter algo =
   let enter_frame_to_push_then_pop instr =
     match instr.it with
-    (* TODO: fix *)
-    (* | EnterI (
-      ({ it = FrameE (Some e_arity, _); _ } as e_frame),
+    | EnterI (
+      ({ it = CaseE ([{ it = Atom.Atom "FRAME_"; _ }] :: _, [e_arity; _]); _ } as e_frame),
       { it = CatE (instrs, { it = ListE ([ { it = CaseE ([[{ it = Atom.Atom "FRAME_"; _ }]], []); _ } ]); _ }); _ },
       il) ->
         begin match e_arity.it with
@@ -1037,11 +1036,6 @@ let remove_enter algo =
             pushI e_tmp ~at:instr.at;
           ]
         end
-    | EnterI (
-      ({ it = FrameE (None, _); _ } as e_frame),
-      { it = ListE ([ { it = CaseE ([[{ it = Atom.Atom "FRAME_"; _ }]], []); _ } ]); _ },
-      il) ->
-        pushI e_frame ~at:instr.at :: il @ [ popI e_frame ~at:instr.at ] *)
     | _ -> [ instr ]
   in
 

From c447847a3a23888a3f1b80ea6cd56083da2d8a27 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Thu, 29 Aug 2024 20:41:25 +0900
Subject: [PATCH 4/5] Don't require popping all values before checking context
 kind

---
 spectec/src/al/ast.ml                         |    2 +-
 spectec/src/backend-interpreter/ds.ml         |    5 +-
 spectec/src/backend-interpreter/ds.mli        |    2 +-
 .../src/backend-interpreter/interpreter.ml    |    7 +-
 spectec/src/backend-prose/print.ml            |    2 +-
 spectec/src/backend-prose/render.ml           |    2 +-
 spectec/src/il2al/translate.ml                |    8 +-
 spectec/test-frontend/TEST.md                 |    6 +
 spectec/test-latex/TEST.md                    |    3 +
 spectec/test-middlend/TEST.md                 |   24 +
 spectec/test-prose/TEST.md                    | 1297 ++++++++---------
 spectec/test-splice/TEST.md                   |    3 +-
 12 files changed, 621 insertions(+), 740 deletions(-)

diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index 8a7149295a..dfd03338d1 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -103,7 +103,7 @@ and expr' =
   (* Conditions *)
   | IsCaseOfE of expr * atom                      (* expr is of the case atom *)
   | IsValidE of expr                              (* expr is valid *)
-  | ContextKindE of atom                          (* "the top of the stack is a" atom *)
+  | ContextKindE of atom                          (* "the fisrt non-value entry of the stack is a" atom *)
   | IsDefinedE of expr                            (* expr is defined *)
   | MatchE of expr * expr                         (* expr matches expr *)
   | HasTypeE of expr * typ                        (* the type of expr is ty *)
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
index bcc09757ba..dfd275fcfc 100644
--- a/spectec/src/backend-interpreter/ds.ml
+++ b/spectec/src/backend-interpreter/ds.ml
@@ -270,9 +270,8 @@ module WasmContext = struct
     | None -> failwith "Wasm context stack underflow"
 
   let get_top_context () =
-    let ctx, vs, _ = get_context () in
-    if List.length vs = 0 then Some ctx 
-    else None
+    let ctx, _, _ = get_context () in
+    ctx
 
   let get_current_context typ =
     let match_context = function
diff --git a/spectec/src/backend-interpreter/ds.mli b/spectec/src/backend-interpreter/ds.mli
index da6c4272cb..34c4054f5e 100644
--- a/spectec/src/backend-interpreter/ds.mli
+++ b/spectec/src/backend-interpreter/ds.mli
@@ -68,7 +68,7 @@ module WasmContext : sig
   val string_of_context : t -> string
   val string_of_context_stack : unit -> string
 
-  val get_top_context : unit -> value option
+  val get_top_context : unit -> value
   val get_current_context : id -> value
   val get_module_instance : unit -> value
 
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 98ae316814..b0537ae310 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -297,10 +297,7 @@ and eval_expr env expr =
   | OptE opt -> Option.map (eval_expr env) opt |> optV
   | TupE el -> List.map (eval_expr env) el |> tupV
   (* Context *)
-  | GetCurContextE None ->
-    (match WasmContext.get_top_context () with
-    | None -> fail_expr expr "cannot get the current context"
-    | Some ctxt -> ctxt)
+  | GetCurContextE None -> WasmContext.get_top_context ()
   | GetCurContextE (Some { it = Atom a; _ }) when List.mem a context_names ->
     WasmContext.get_current_context a
   | ChooseE e ->
@@ -337,7 +334,7 @@ and eval_expr env expr =
   | ContextKindE a ->
     let ctx = WasmContext.get_top_context () in
     (match a.it, ctx with
-    | Atom case, Some (CaseV (case', _)) -> boolV (case = case')
+    | Atom case, CaseV (case', _) -> boolV (case = case')
     | _ -> boolV false)
   | IsDefinedE e ->
     e
diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml
index 07505129c7..3dfaad1eed 100644
--- a/spectec/src/backend-prose/print.ml
+++ b/spectec/src/backend-prose/print.ml
@@ -161,7 +161,7 @@ and string_of_expr expr =
     )
   | OptE (Some e) -> "?(" ^ string_of_expr e ^ ")"
   | OptE None -> "?()"
-  | ContextKindE a -> sprintf "the top of the stack is a %s" (string_of_atom a)
+  | ContextKindE a -> sprintf "the first non-value entry of the stack is a %s" (string_of_atom a)
   | IsDefinedE e -> sprintf "%s is defined" (string_of_expr e)
   | IsCaseOfE (e, a) -> sprintf "%s is of the case %s" (string_of_expr e) (string_of_atom a)
   | HasTypeE (e, t) -> sprintf "the type of %s is %s" (string_of_expr e) (string_of_typ t)
diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index f863d2fea1..19559029e1 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -416,7 +416,7 @@ and render_expr' env expr =
     sprintf "an element of %s" se
   | Al.Ast.ContextKindE a ->
     let sa = render_atom env a in
-    sprintf "the top of the stack is a %s" sa
+    sprintf "the first non-value entry of the stack is a %s" sa
   | Al.Ast.IsDefinedE e ->
     let se = render_expr env e in
     sprintf "%s is defined" se
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index ce03168384..e36e5f080d 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -1106,17 +1106,11 @@ let rec translate_rgroup' (rule: rule_def) =
   let ctxt_block = match ctxt_blocks with
   | [] -> []
   | _ ->
-    let valTs = listT valT in
-    let e_vals = iterE (subE ("val", valT) ~note:valT, [ "val" ], List) ~note:valTs in
-    let instr_popall = popAllI e_vals in
-    let instr_push = pushI e_vals in
-
-    instr_popall ::
     List.fold_right (fun instrs acc ->
       assert (List.length instrs = 1);
       let if_instr = List.hd instrs in
       match if_instr.it with
-      | IfI (c, instrs1, []) -> [{if_instr with it = IfI (c, instr_push :: instrs1, acc)}]
+      | IfI (c, instrs1, []) -> [{if_instr with it = IfI (c, instrs1, acc)}]
       | _ -> assert false
     ) (List.map snd ctxt_blocks) throw_block
   in
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 1a2851221a..4c55cac96f 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -3325,6 +3325,12 @@ syntax state =
 syntax config =
   | `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)
 
+;; 4-runtime.watsup
+syntax evalctx =
+  | `LABEL_%{%}`{n : n, instr* : instr*}(n : n, instr*{instr : instr} : instr*)
+  | `FRAME_%{%}`{n : n, frame : frame}(n : n, frame : frame)
+  | `HANDLER_%{%}`{n : n, catch* : catch*}(n : n, catch*{catch : catch} : catch*)
+
 ;; 5-runtime-aux.watsup
 def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
   ;; 5-runtime-aux.watsup
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 53a6405158..198cbac649 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -4056,6 +4056,9 @@ $$
 {{\mathsf{frame}}_{n}}{\{ {\mathit{frame}} \}}~{{\mathit{instr}}^\ast} \\ &&|&
 {{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}}^\ast} \\ &&|&
 \mathsf{trap} \\
+\mbox{(evaluation context)} & {\mathit{evalctx}} &::=& {{\mathsf{label}}_{n}}{\{ {{\mathit{instr}}^\ast} \}} \\ &&|&
+{{\mathsf{frame}}_{n}}{\{ {\mathit{frame}} \}} \\ &&|&
+{{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}} \\
 \end{array}
 $$
 
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 15d6fce661..769d107af7 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -3315,6 +3315,12 @@ syntax state =
 syntax config =
   | `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)
 
+;; 4-runtime.watsup
+syntax evalctx =
+  | `LABEL_%{%}`{n : n, instr* : instr*}(n : n, instr*{instr : instr} : instr*)
+  | `FRAME_%{%}`{n : n, frame : frame}(n : n, frame : frame)
+  | `HANDLER_%{%}`{n : n, catch* : catch*}(n : n, catch*{catch : catch} : catch*)
+
 ;; 5-runtime-aux.watsup
 def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
   ;; 5-runtime-aux.watsup
@@ -11700,6 +11706,12 @@ syntax state =
 syntax config =
   | `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)
 
+;; 4-runtime.watsup
+syntax evalctx =
+  | `LABEL_%{%}`{n : n, instr* : instr*}(n : n, instr*{instr : instr} : instr*)
+  | `FRAME_%{%}`{n : n, frame : frame}(n : n, frame : frame)
+  | `HANDLER_%{%}`{n : n, catch* : catch*}(n : n, catch*{catch : catch} : catch*)
+
 ;; 5-runtime-aux.watsup
 def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
   ;; 5-runtime-aux.watsup
@@ -20087,6 +20099,12 @@ syntax state =
 syntax config =
   | `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)
 
+;; 4-runtime.watsup
+syntax evalctx =
+  | `LABEL_%{%}`{n : n, instr* : instr*}(n : n, instr*{instr : instr} : instr*)
+  | `FRAME_%{%}`{n : n, frame : frame}(n : n, frame : frame)
+  | `HANDLER_%{%}`{n : n, catch* : catch*}(n : n, catch*{catch : catch} : catch*)
+
 ;; 5-runtime-aux.watsup
 def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
   ;; 5-runtime-aux.watsup
@@ -28474,6 +28492,12 @@ syntax state =
 syntax config =
   | `%;%`{state : state, instr* : instr*}(state : state, instr*{instr : instr} : instr*)
 
+;; 4-runtime.watsup
+syntax evalctx =
+  | `LABEL_%{%}`{n : n, instr* : instr*}(n : n, instr*{instr : instr} : instr*)
+  | `FRAME_%{%}`{n : n, frame : frame}(n : n, frame : frame)
+  | `HANDLER_%{%}`{n : n, catch* : catch*}(n : n, catch*{catch : catch} : catch*)
+
 ;; 5-runtime-aux.watsup
 def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype
   ;; 5-runtime-aux.watsup
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 151aa61e80..0eae22001b 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -679,11 +679,13 @@ watsup 0.4 generator
 ......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+
+#. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Assert: Due to validation, a label is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{label}`.
 
-#. Pop the current label from the stack.
+#. Pop the current :math:`\mathsf{label}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -692,17 +694,9 @@ watsup 0.4 generator
 .............................................................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. Assert: Due to validation, the top of the stack is a :math:`\mathsf{label}`.
-
-#. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-#. Let :math:`L` be the current label.
-
-#. Let :math:`n` be the arity of :math:`L`.
+1. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{label}`.
 
-#. Let :math:`{{\mathit{instr}'}^\ast}` be the continuation of :math:`L`.
+#. Let :math:`({{\mathsf{label}}_{n}}{\{}~{{\mathit{instr}'}^\ast}~\})` be the current :math:`\mathsf{label}` context.
 
 #. If :math:`n_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`0`, then:
 
@@ -712,7 +706,7 @@ watsup 0.4 generator
 
    #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -726,7 +720,7 @@ watsup 0.4 generator
 
       1) Let :math:`l` be :math:`n_{\mathit{u{\kern-0.1em\scriptstyle 0}}} - 1`.
 
-      #) Pop the current label from the stack.
+      #) Pop the current :math:`\mathsf{label}` context from the stack.
 
       #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -771,9 +765,7 @@ watsup 0.4 generator
 ......................
 
 
-1. Let :math:`f` be the current frame.
-
-#. Let :math:`n` be the arity of :math:`f`.
+1. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -781,9 +773,9 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{n}}` from the stack.
 
-#. Assert: Due to validation, a frame is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{frame}`.
 
-#. Pop the current frame from the stack.
+#. Pop the current :math:`\mathsf{frame}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -792,15 +784,9 @@ watsup 0.4 generator
 .......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. If the top of the stack is a :math:`\mathsf{frame}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-   #. Let :math:`f` be the current frame.
+1. If the first non-value entry of the stack is a :math:`\mathsf{frame}`, then:
 
-   #. Let :math:`n` be the arity of :math:`f`.
+   a. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
    #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -808,17 +794,15 @@ watsup 0.4 generator
 
    #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-   #. Pop the current frame from the stack.
+   #. Pop the current :math:`\mathsf{frame}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
-#. Else if the top of the stack is a :math:`\mathsf{label}`, then:
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -943,26 +927,20 @@ watsup 0.4 generator
 
 #. If :math:`{t^?}` is not defined, then:
 
-   a. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-   #. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+   a. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 #. Let :math:`n` be :math:`1`.
 
 #. If :math:`{t^?}` is not :math:`\epsilon`, then:
 
-   a. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-   #. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+   a. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{loop}~{t^?}~{{\mathit{instr}}^\ast}`
 ...................................................
 
 
-1. Let :math:`L` be the label whose arity is :math:`0` and whose continuation is :math:`(\mathsf{loop}~{t^?}~{{\mathit{instr}}^\ast})`.
-
-#. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+1. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{0}}{\{}~(\mathsf{loop}~{t^?}~{{\mathit{instr}}^\ast})~\})`.
 
 
 :math:`\mathsf{call}~x`
@@ -1031,13 +1009,9 @@ watsup 0.4 generator
 
 #. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~{{\mathit{val}}^{k}}~{{{\mathrm{default}}}_{t}^\ast},\; \mathsf{module}~{\mathit{mm}} \}\end{array}`.
 
-#. Let :math:`F` be the activation of :math:`f` with arity :math:`n`.
-
-#. Push :math:`F` to the stack.
+#. Push the value :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` to the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-#. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{local{.}get}~x`
@@ -2132,7 +2106,7 @@ watsup 0.4 generator
 ........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f`.
 
@@ -2141,7 +2115,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{funcs}`.
 
@@ -2178,7 +2152,7 @@ watsup 0.4 generator
 .............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -2187,7 +2161,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{types}{}[x]`.
 
@@ -2196,7 +2170,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{funcs}{}[f{.}\mathsf{module}{.}\mathsf{funcs}{}[x]]`.
 
@@ -2205,7 +2179,7 @@ watsup 0.4 generator
 ............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]`.
 
@@ -2214,7 +2188,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]`.
 
@@ -2223,7 +2197,7 @@ watsup 0.4 generator
 .........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]`.
 
@@ -2232,7 +2206,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{locals}{}[x]`.
 
@@ -2241,7 +2215,7 @@ watsup 0.4 generator
 ..............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`f{.}\mathsf{locals}{}[x]` with :math:`v`.
 
@@ -2250,7 +2224,7 @@ watsup 0.4 generator
 ...............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]{.}\mathsf{value}` with :math:`v`.
 
@@ -2259,7 +2233,7 @@ watsup 0.4 generator
 .................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]{.}\mathsf{refs}{}[i]` with :math:`a`.
 
@@ -2268,7 +2242,7 @@ watsup 0.4 generator
 ..............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]` with :math:`{\mathit{ti}}`.
 
@@ -2277,7 +2251,7 @@ watsup 0.4 generator
 .........................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]{.}\mathsf{bytes}{}[i : j]` with :math:`{b^\ast}`.
 
@@ -2286,7 +2260,7 @@ watsup 0.4 generator
 ............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]` with :math:`{\mathit{mi}}`.
 
@@ -2711,23 +2685,23 @@ watsup 0.4 generator
 
 #. Let :math:`z` be :math:`f_{\mathit{init}}`.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~z~\})` to the stack.
 
 #. Let :math:`{(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i_{\mathsf{d}})^\ast}` be :math:`{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{d}})^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~z~\})` to the stack.
 
 #. Let :math:`{(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i_{\mathsf{e}})^\ast}` be :math:`{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{e}})^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~z~\})` to the stack.
 
 #. Let :math:`{{\mathit{val}}^\ast}` be :math:`{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{g}})^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Let :math:`{\mathit{moduleinst}}` be :math:`{\mathrm{allocmodule}}({\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}^\ast})`.
 
@@ -2737,13 +2711,13 @@ watsup 0.4 generator
 
 #. Perform :math:`{\mathrm{initdata}}({\mathit{moduleinst}}, {i_{\mathsf{d}}^\ast}, {{b^\ast}^\ast})`.
 
-#. Push the activation of :math:`f` with arity :math:`0` to the stack.
+#. Push the evaluation context :math:`({\mathsf{frame}}_{0}\,\{~f~\})` to the stack.
 
 #. If :math:`{(\mathsf{call}~{x'})^?}` is defined, then:
 
    a. Execute the instruction :math:`(\mathsf{call}~{x'})`.
 
-#. Pop the activation of :math:`f` with arity :math:`0` from the stack.
+#. Pop the evaluation context :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -2754,15 +2728,15 @@ watsup 0.4 generator
 
 1. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~\epsilon,\; \mathsf{module}~\{ \begin{array}[t]{@{}l@{}}\mathsf{types}~\epsilon,\; \mathsf{funcs}~\epsilon,\; \mathsf{globals}~\epsilon,\; \mathsf{tables}~\epsilon,\; \mathsf{mems}~\epsilon,\; \mathsf{exports}~\epsilon \}\end{array} \}\end{array}`.
 
-#. Push the activation of :math:`f` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` to the stack.
 
 #. Let :math:`({t_1^{n}}~\rightarrow~{t_2^\ast})` be :math:`z{.}\mathsf{funcs}{}[{\mathit{fa}}]{.}\mathsf{type}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Let :math:`k` be :math:`{|{t_2^\ast}|}`.
 
-#. Push the activation of :math:`f` with arity :math:`k` to the stack.
+#. Push the evaluation context :math:`({\mathsf{frame}}_{k}\,\{~f~\})` to the stack.
 
 #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -2770,7 +2744,7 @@ watsup 0.4 generator
 
 #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Pop the activation of :math:`f` with arity :math:`k` from the stack.
+#. Pop the evaluation context :math:`({\mathsf{frame}}_{k}\,\{~f~\})` from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -3196,30 +3170,27 @@ Step_pure/if t? instr_1* instr_2*
   a. Execute the instruction (BLOCK t? instr_2*).
 
 Step_pure/label
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, a label is now on the top of the stack.
-3. Pop the current label from the stack.
-4. Push the values val* to the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+2. Pop all values val* from the top of the stack.
+3. Assert: Due to validation, the first non-value entry of the stack is a LABEL_.
+4. Pop the current LABEL_ context from the stack.
+5. Push the values val* to the stack.
 
 Step_pure/br n_u0
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, the top of the stack is a LABEL_.
-3. Push the values val* to the stack.
-4. Let L be the current label.
-5. Let n be the arity of L.
-6. Let instr'* be the continuation of L.
-7. If (n_u0 is 0), then:
+1. Assert: Due to validation, the first non-value entry of the stack is a LABEL_.
+2. Let (LABEL_ n { instr'* }) be the current LABEL_ context.
+3. If (n_u0 is 0), then:
   a. Assert: Due to validation, there are at least n values on the top of the stack.
   b. Pop the values val^n from the stack.
   c. Pop all values val'* from the top of the stack.
-  d. Pop the current label from the stack.
+  d. Pop the current LABEL_ context from the stack.
   e. Push the values val^n to the stack.
   f. Execute the instruction instr'*.
-8. Else:
+4. Else:
   a. Pop all values val* from the top of the stack.
   b. If (n_u0 ≥ 1), then:
     1) Let l be (n_u0 - 1).
-    2) Pop the current label from the stack.
+    2) Pop the current LABEL_ context from the stack.
     3) Push the values val* to the stack.
     4) Execute the instruction (BR l).
 
@@ -3240,32 +3211,27 @@ Step_pure/br_table l* l'
   a. Execute the instruction (BR l').
 
 Step_pure/frame
-1. Let f be the current frame.
-2. Let n be the arity of f.
+1. Let (FRAME_ n { f }) be the current FRAME_ context.
+2. Assert: Due to validation, there are at least n values on the top of the stack.
 3. Assert: Due to validation, there are at least n values on the top of the stack.
-4. Assert: Due to validation, there are at least n values on the top of the stack.
-5. Pop the values val^n from the stack.
-6. Assert: Due to validation, a frame is now on the top of the stack.
-7. Pop the current frame from the stack.
-8. Push the values val^n to the stack.
+4. Pop the values val^n from the stack.
+5. Assert: Due to validation, the first non-value entry of the stack is a FRAME_.
+6. Pop the current FRAME_ context from the stack.
+7. Push the values val^n to the stack.
 
 Step_pure/return
-1. Pop all values val* from the top of the stack.
-2. If the top of the stack is a FRAME_, then:
-  a. Push the values val* to the stack.
-  b. Let f be the current frame.
-  c. Let n be the arity of f.
-  d. Assert: Due to validation, there are at least n values on the top of the stack.
-  e. Pop the values val^n from the stack.
-  f. Pop all values val'* from the top of the stack.
-  g. Pop the current frame from the stack.
-  h. Push the values val^n to the stack.
-3. Else if the top of the stack is a LABEL_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Pop the current label from the stack.
-  d. Push the values val* to the stack.
-  e. Execute the instruction RETURN.
+1. If the first non-value entry of the stack is a FRAME_, then:
+  a. Let (FRAME_ n { f }) be the current FRAME_ context.
+  b. Assert: Due to validation, there are at least n values on the top of the stack.
+  c. Pop the values val^n from the stack.
+  d. Pop all values val'* from the top of the stack.
+  e. Pop the current FRAME_ context from the stack.
+  f. Push the values val^n to the stack.
+2. Else if the first non-value entry of the stack is a LABEL_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current LABEL_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction RETURN.
 
 Step_pure/unop t unop
 1. Assert: Due to validation, a value of value type valtype_0 is on the top of the stack.
@@ -3322,16 +3288,13 @@ Step_pure/local.tee x
 Step_read/block t? instr*
 1. Let n be 0.
 2. If t? is not defined, then:
-  a. Let L be the label_n{[]}.
-  b. Enter instr* with label L.
+  a. Enter instr* with label (LABEL_ n { [] }).
 3. Let n be 1.
 4. If (t? is not ?()), then:
-  a. Let L be the label_n{[]}.
-  b. Enter instr* with label L.
+  a. Enter instr* with label (LABEL_ n { [] }).
 
 Step_read/loop t? instr*
-1. Let L be the label_0{[(LOOP t? instr*)]}.
-2. Enter instr* with label L.
+1. Enter instr* with label (LABEL_ 0 { [(LOOP t? instr*)] }).
 
 Step_read/call x
 1. Let z be the current state.
@@ -3364,10 +3327,8 @@ Step_read/call_addr a
 8. Assert: Due to validation, local_0 is of the case LOCAL.
 9. Let (LOCAL t)* be local_0.
 10. Let f be { LOCALS: val^k :: $default_(t)*; MODULE: mm; }.
-11. Let F be the activation of f with arity n.
-12. Push F to the stack.
-13. Let L be the label_n{[]}.
-14. Enter instr* with label L.
+11. Push the value (FRAME_ n { f }) to the stack.
+12. Enter instr* with label (LABEL_ n { [] }).
 
 Step_read/local.get x
 1. Let z be the current state.
@@ -3893,11 +3854,11 @@ store
 1. Return.
 
 frame
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.
 
 funcaddr
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.FUNCS.
 
 funcinst
@@ -3913,55 +3874,55 @@ meminst
 1. Return s.MEMS.
 
 moduleinst
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.
 
 type x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.TYPES[x].
 
 func x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.FUNCS[f.MODULE.FUNCS[x]].
 
 global x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.GLOBALS[f.MODULE.GLOBALS[x]].
 
 table x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.TABLES[f.MODULE.TABLES[x]].
 
 mem x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.MEMS[f.MODULE.MEMS[x]].
 
 local x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.LOCALS[x].
 
 with_local x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace f.LOCALS[x] with v.
 
 with_global x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.GLOBALS[f.MODULE.GLOBALS[x]].VALUE with v.
 
 with_table x i a
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]].REFS[i] with ?(a).
 
 with_tableinst x ti
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]] with ti.
 
 with_mem x i j b*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] with b*.
 
 with_meminst x mi
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]] with mi.
 
 growtable ti n
@@ -4164,36 +4125,36 @@ instantiate z module externaddr*
 14. Let moduleinst_init be { TYPES: functype*; FUNCS: $funcs(externaddr*) :: (|s.FUNCS| + i_F)^(i_F<n_F); GLOBALS: $globals(externaddr*); TABLES: []; MEMS: []; EXPORTS: []; }.
 15. Let f_init be { LOCALS: []; MODULE: moduleinst_init; }.
 16. Let z be f_init.
-17. Push the activation of z to the stack.
+17. Push the value (FRAME_ 0 { z }) to the stack.
 18. Let [(I32.CONST i_D)]* be $eval_expr(expr_D)*.
-19. Pop the activation of _f from the stack.
-20. Push the activation of z to the stack.
+19. Pop the value (FRAME_ 0 { _f }) from the stack.
+20. Push the value (FRAME_ 0 { z }) to the stack.
 21. Let [(I32.CONST i_E)]* be $eval_expr(expr_E)*.
-22. Pop the activation of _f from the stack.
-23. Push the activation of z to the stack.
+22. Pop the value (FRAME_ 0 { _f }) from the stack.
+23. Push the value (FRAME_ 0 { z }) to the stack.
 24. Let [val]* be $eval_expr(expr_G)*.
-25. Pop the activation of _f from the stack.
+25. Pop the value (FRAME_ 0 { _f }) from the stack.
 26. Let moduleinst be $allocmodule(module, externaddr*, val*).
 27. Let f be { LOCALS: []; MODULE: moduleinst; }.
 28. Perform $initelem(moduleinst, i_E*, moduleinst.FUNCS[x]**).
 29. Perform $initdata(moduleinst, i_D*, b**).
-30. Push the activation of f with arity 0 to the stack.
+30. Push the evaluation context (FRAME_ 0 { f }) to the stack.
 31. If (CALL x')? is defined, then:
   a. Execute the instruction (CALL x').
-32. Pop the activation of f with arity 0 from the stack.
+32. Pop the evaluation context (FRAME_ 0 { f }) from the stack.
 33. Return f.MODULE.
 
 invoke z fa val^n
 1. Let f be { LOCALS: []; MODULE: { TYPES: []; FUNCS: []; GLOBALS: []; TABLES: []; MEMS: []; EXPORTS: []; }; }.
-2. Push the activation of f to the stack.
+2. Push the value (FRAME_ 0 { f }) to the stack.
 3. Let (t_1^n -> t_2*) be $funcinst(z)[fa].TYPE.
-4. Pop the activation of _f from the stack.
+4. Pop the value (FRAME_ 0 { _f }) from the stack.
 5. Let k be |t_2*|.
-6. Push the activation of f with arity k to the stack.
+6. Push the evaluation context (FRAME_ k { f }) to the stack.
 7. Push the values val^n to the stack.
 8. Execute the instruction (CALL_ADDR fa).
 9. Pop all values val* from the top of the stack.
-10. Pop the activation of f with arity k from the stack.
+10. Pop the evaluation context (FRAME_ k { f }) from the stack.
 11. Push the values val* to the stack.
 12. Pop the values val^k from the stack.
 13. Return val^k.
@@ -5246,11 +5207,13 @@ watsup 0.4 generator
 ......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+
+#. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Assert: Due to validation, a label is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{label}`.
 
-#. Pop the current label from the stack.
+#. Pop the current :math:`\mathsf{label}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -5259,17 +5222,9 @@ watsup 0.4 generator
 .............................................................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. Assert: Due to validation, the top of the stack is a :math:`\mathsf{label}`.
-
-#. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-#. Let :math:`L` be the current label.
-
-#. Let :math:`n` be the arity of :math:`L`.
+1. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{label}`.
 
-#. Let :math:`{{\mathit{instr}'}^\ast}` be the continuation of :math:`L`.
+#. Let :math:`({{\mathsf{label}}_{n}}{\{}~{{\mathit{instr}'}^\ast}~\})` be the current :math:`\mathsf{label}` context.
 
 #. If :math:`n_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is :math:`0`, then:
 
@@ -5279,7 +5234,7 @@ watsup 0.4 generator
 
    #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -5293,7 +5248,7 @@ watsup 0.4 generator
 
       1) Let :math:`l` be :math:`n_{\mathit{u{\kern-0.1em\scriptstyle 0}}} - 1`.
 
-      #) Pop the current label from the stack.
+      #) Pop the current :math:`\mathsf{label}` context from the stack.
 
       #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -5338,9 +5293,7 @@ watsup 0.4 generator
 ......................
 
 
-1. Let :math:`f` be the current frame.
-
-#. Let :math:`n` be the arity of :math:`f`.
+1. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -5348,9 +5301,9 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{n}}` from the stack.
 
-#. Assert: Due to validation, a frame is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{frame}`.
 
-#. Pop the current frame from the stack.
+#. Pop the current :math:`\mathsf{frame}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -5359,15 +5312,9 @@ watsup 0.4 generator
 .......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. If the top of the stack is a :math:`\mathsf{frame}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+1. If the first non-value entry of the stack is a :math:`\mathsf{frame}`, then:
 
-   #. Let :math:`f` be the current frame.
-
-   #. Let :math:`n` be the arity of :math:`f`.
+   a. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
    #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -5375,17 +5322,15 @@ watsup 0.4 generator
 
    #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-   #. Pop the current frame from the stack.
+   #. Pop the current :math:`\mathsf{frame}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
-#. Else if the top of the stack is a :math:`\mathsf{label}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -5952,9 +5897,7 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{k}}` from the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-#. Enter :math:`{{\mathit{val}}^{k}}~{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{val}}^{k}}~{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast}`
@@ -5969,9 +5912,7 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{k}}` from the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`k` and whose continuation is :math:`(\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast})`.
-
-#. Enter :math:`{{\mathit{val}}^{k}}~{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{val}}^{k}}~{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{k}}{\{}~(\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast})~\})`.
 
 
 :math:`\mathsf{call}~x`
@@ -6040,13 +5981,9 @@ watsup 0.4 generator
 
 #. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~{{\mathit{val}}^{k}}~{{{\mathrm{default}}}_{t}^\ast},\; \mathsf{module}~{\mathit{mm}} \}\end{array}`.
 
-#. Let :math:`F` be the activation of :math:`f` with arity :math:`n`.
-
-#. Push :math:`F` to the stack.
+#. Push the value :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` to the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-#. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{ref{.}func}~x`
@@ -8800,7 +8737,7 @@ watsup 0.4 generator
 ........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f`.
 
@@ -8809,7 +8746,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{funcs}`.
 
@@ -8860,7 +8797,7 @@ watsup 0.4 generator
 .............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -8869,7 +8806,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{types}{}[x]`.
 
@@ -8878,7 +8815,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{funcs}{}[f{.}\mathsf{module}{.}\mathsf{funcs}{}[x]]`.
 
@@ -8887,7 +8824,7 @@ watsup 0.4 generator
 ............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]`.
 
@@ -8896,7 +8833,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]`.
 
@@ -8905,7 +8842,7 @@ watsup 0.4 generator
 .........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]`.
 
@@ -8914,7 +8851,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{elems}{}[f{.}\mathsf{module}{.}\mathsf{elems}{}[x]]`.
 
@@ -8923,7 +8860,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{datas}{}[f{.}\mathsf{module}{.}\mathsf{datas}{}[x]]`.
 
@@ -8932,7 +8869,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{locals}{}[x]`.
 
@@ -8941,7 +8878,7 @@ watsup 0.4 generator
 ..............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`f{.}\mathsf{locals}{}[x]` with :math:`v`.
 
@@ -8950,7 +8887,7 @@ watsup 0.4 generator
 ...............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]{.}\mathsf{value}` with :math:`v`.
 
@@ -8959,7 +8896,7 @@ watsup 0.4 generator
 .................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]{.}\mathsf{refs}{}[i]` with :math:`r`.
 
@@ -8968,7 +8905,7 @@ watsup 0.4 generator
 ..............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]` with :math:`{\mathit{ti}}`.
 
@@ -8977,7 +8914,7 @@ watsup 0.4 generator
 .........................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]{.}\mathsf{bytes}{}[i : j]` with :math:`{b^\ast}`.
 
@@ -8986,7 +8923,7 @@ watsup 0.4 generator
 ............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]` with :math:`{\mathit{mi}}`.
 
@@ -8995,7 +8932,7 @@ watsup 0.4 generator
 ....................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{elems}{}[f{.}\mathsf{module}{.}\mathsf{elems}{}[x]]{.}\mathsf{refs}` with :math:`{r^\ast}`.
 
@@ -9004,7 +8941,7 @@ watsup 0.4 generator
 ....................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({\mathsf{frame}}_{}\,\{~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{datas}{}[f{.}\mathsf{module}{.}\mathsf{datas}{}[x]]{.}\mathsf{bytes}` with :math:`{b^\ast}`.
 
@@ -9538,23 +9475,23 @@ watsup 0.4 generator
 
 #. Let :math:`z` be :math:`f_{\mathit{init}}`.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~z~\})` to the stack.
 
 #. Let :math:`{{\mathit{val}}^\ast}` be :math:`{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{g}})^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~z~\})` to the stack.
 
 #. Let :math:`{{{\mathit{ref}}^\ast}^\ast}` be :math:`{{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{e}})^\ast}^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Let :math:`{\mathit{moduleinst}}` be :math:`{\mathrm{allocmodule}}({\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}^\ast}, {{{\mathit{ref}}^\ast}^\ast})`.
 
 #. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~\epsilon,\; \mathsf{module}~{\mathit{moduleinst}} \}\end{array}`.
 
-#. Push the activation of :math:`f` with arity :math:`0` to the stack.
+#. Push the evaluation context :math:`({\mathsf{frame}}_{0}\,\{~f~\})` to the stack.
 
 #. Execute the sequence :math:`{{\mathit{instr}}_{\mathsf{e}}^\ast}`.
 
@@ -9564,7 +9501,7 @@ watsup 0.4 generator
 
    a. Execute the instruction :math:`(\mathsf{call}~x)`.
 
-#. Pop the activation of :math:`f` with arity :math:`0` from the stack.
+#. Pop the evaluation context :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -9575,15 +9512,15 @@ watsup 0.4 generator
 
 1. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~\epsilon,\; \mathsf{module}~\{ \begin{array}[t]{@{}l@{}}\mathsf{types}~\epsilon,\; \mathsf{funcs}~\epsilon,\; \mathsf{globals}~\epsilon,\; \mathsf{tables}~\epsilon,\; \mathsf{mems}~\epsilon,\; \mathsf{elems}~\epsilon,\; \mathsf{datas}~\epsilon,\; \mathsf{exports}~\epsilon \}\end{array} \}\end{array}`.
 
-#. Push the activation of :math:`f` to the stack.
+#. Push the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` to the stack.
 
 #. Let :math:`({t_1^{n}}~\rightarrow~{t_2^\ast})` be :math:`z{.}\mathsf{funcs}{}[{\mathit{fa}}]{.}\mathsf{type}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({\mathsf{frame}}_{0}\,\{~f~\})` from the stack.
 
 #. Let :math:`k` be :math:`{|{t_2^\ast}|}`.
 
-#. Push the activation of :math:`f` with arity :math:`k` to the stack.
+#. Push the evaluation context :math:`({\mathsf{frame}}_{k}\,\{~f~\})` to the stack.
 
 #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -9591,7 +9528,7 @@ watsup 0.4 generator
 
 #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Pop the activation of :math:`f` with arity :math:`k` from the stack.
+#. Pop the evaluation context :math:`({\mathsf{frame}}_{k}\,\{~f~\})` from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -10261,30 +10198,27 @@ Step_pure/if bt instr_1* instr_2*
   a. Execute the instruction (BLOCK bt instr_2*).
 
 Step_pure/label
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, a label is now on the top of the stack.
-3. Pop the current label from the stack.
-4. Push the values val* to the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+2. Pop all values val* from the top of the stack.
+3. Assert: Due to validation, the first non-value entry of the stack is a LABEL_.
+4. Pop the current LABEL_ context from the stack.
+5. Push the values val* to the stack.
 
 Step_pure/br n_u0
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, the top of the stack is a LABEL_.
-3. Push the values val* to the stack.
-4. Let L be the current label.
-5. Let n be the arity of L.
-6. Let instr'* be the continuation of L.
-7. If (n_u0 is 0), then:
+1. Assert: Due to validation, the first non-value entry of the stack is a LABEL_.
+2. Let (LABEL_ n { instr'* }) be the current LABEL_ context.
+3. If (n_u0 is 0), then:
   a. Assert: Due to validation, there are at least n values on the top of the stack.
   b. Pop the values val^n from the stack.
   c. Pop all values val'* from the top of the stack.
-  d. Pop the current label from the stack.
+  d. Pop the current LABEL_ context from the stack.
   e. Push the values val^n to the stack.
   f. Execute the instruction instr'*.
-8. Else:
+4. Else:
   a. Pop all values val* from the top of the stack.
   b. If (n_u0 ≥ 1), then:
     1) Let l be (n_u0 - 1).
-    2) Pop the current label from the stack.
+    2) Pop the current LABEL_ context from the stack.
     3) Push the values val* to the stack.
     4) Execute the instruction (BR l).
 
@@ -10305,32 +10239,27 @@ Step_pure/br_table l* l'
   a. Execute the instruction (BR l').
 
 Step_pure/frame
-1. Let f be the current frame.
-2. Let n be the arity of f.
+1. Let (FRAME_ n { f }) be the current FRAME_ context.
+2. Assert: Due to validation, there are at least n values on the top of the stack.
 3. Assert: Due to validation, there are at least n values on the top of the stack.
-4. Assert: Due to validation, there are at least n values on the top of the stack.
-5. Pop the values val^n from the stack.
-6. Assert: Due to validation, a frame is now on the top of the stack.
-7. Pop the current frame from the stack.
-8. Push the values val^n to the stack.
+4. Pop the values val^n from the stack.
+5. Assert: Due to validation, the first non-value entry of the stack is a FRAME_.
+6. Pop the current FRAME_ context from the stack.
+7. Push the values val^n to the stack.
 
 Step_pure/return
-1. Pop all values val* from the top of the stack.
-2. If the top of the stack is a FRAME_, then:
-  a. Push the values val* to the stack.
-  b. Let f be the current frame.
-  c. Let n be the arity of f.
-  d. Assert: Due to validation, there are at least n values on the top of the stack.
-  e. Pop the values val^n from the stack.
-  f. Pop all values val'* from the top of the stack.
-  g. Pop the current frame from the stack.
-  h. Push the values val^n to the stack.
-3. Else if the top of the stack is a LABEL_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Pop the current label from the stack.
-  d. Push the values val* to the stack.
-  e. Execute the instruction RETURN.
+1. If the first non-value entry of the stack is a FRAME_, then:
+  a. Let (FRAME_ n { f }) be the current FRAME_ context.
+  b. Assert: Due to validation, there are at least n values on the top of the stack.
+  c. Pop the values val^n from the stack.
+  d. Pop all values val'* from the top of the stack.
+  e. Pop the current FRAME_ context from the stack.
+  f. Push the values val^n to the stack.
+2. Else if the first non-value entry of the stack is a LABEL_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current LABEL_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction RETURN.
 
 Step_pure/unop nt unop
 1. Assert: Due to validation, a value of value type numtype_0 is on the top of the stack.
@@ -10598,16 +10527,14 @@ Step_read/block bt instr*
 2. Let (t_1^k -> t_2^n) be $blocktype(z, bt).
 3. Assert: Due to validation, there are at least k values on the top of the stack.
 4. Pop the values val^k from the stack.
-5. Let L be the label_n{[]}.
-6. Enter val^k :: instr* with label L.
+5. Enter val^k :: instr* with label (LABEL_ n { [] }).
 
 Step_read/loop bt instr*
 1. Let z be the current state.
 2. Let (t_1^k -> t_2^n) be $blocktype(z, bt).
 3. Assert: Due to validation, there are at least k values on the top of the stack.
 4. Pop the values val^k from the stack.
-5. Let L be the label_k{[(LOOP bt instr*)]}.
-6. Enter val^k :: instr* with label L.
+5. Enter val^k :: instr* with label (LABEL_ k { [(LOOP bt instr*)] }).
 
 Step_read/call x
 1. Let z be the current state.
@@ -10640,10 +10567,8 @@ Step_read/call_addr a
 8. Assert: Due to validation, local_0 is of the case LOCAL.
 9. Let (LOCAL t)* be local_0.
 10. Let f be { LOCALS: val^k :: $default_(t)*; MODULE: mm; }.
-11. Let F be the activation of f with arity n.
-12. Push F to the stack.
-13. Let L be the label_n{[]}.
-14. Enter instr* with label L.
+11. Push the value (FRAME_ n { f }) to the stack.
+12. Enter instr* with label (LABEL_ n { [] }).
 
 Step_read/ref.func x
 1. Let z be the current state.
@@ -11971,11 +11896,11 @@ store
 1. Return.
 
 frame
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.
 
 funcaddr
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.FUNCS.
 
 funcinst
@@ -11997,71 +11922,71 @@ datainst
 1. Return s.DATAS.
 
 moduleinst
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.
 
 type x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.TYPES[x].
 
 func x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.FUNCS[f.MODULE.FUNCS[x]].
 
 global x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.GLOBALS[f.MODULE.GLOBALS[x]].
 
 table x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.TABLES[f.MODULE.TABLES[x]].
 
 mem x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.MEMS[f.MODULE.MEMS[x]].
 
 elem x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.ELEMS[f.MODULE.ELEMS[x]].
 
 data x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.DATAS[f.MODULE.DATAS[x]].
 
 local x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.LOCALS[x].
 
 with_local x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace f.LOCALS[x] with v.
 
 with_global x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.GLOBALS[f.MODULE.GLOBALS[x]].VALUE with v.
 
 with_table x i r
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]].REFS[i] with r.
 
 with_tableinst x ti
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]] with ti.
 
 with_mem x i j b*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] with b*.
 
 with_meminst x mi
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]] with mi.
 
 with_elem x r*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.ELEMS[f.MODULE.ELEMS[x]].REFS with r*.
 
 with_data x b*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.DATAS[f.MODULE.DATAS[x]].BYTES with b*.
 
 growtable ti n r
@@ -12316,33 +12241,33 @@ instantiate z module externaddr*
 16. Let moduleinst_init be { TYPES: functype*; FUNCS: $funcs(externaddr*) :: (|s.FUNCS| + i_F)^(i_F<n_F); GLOBALS: $globals(externaddr*); TABLES: []; MEMS: []; ELEMS: []; DATAS: []; EXPORTS: []; }.
 17. Let f_init be { LOCALS: []; MODULE: moduleinst_init; }.
 18. Let z be f_init.
-19. Push the activation of z to the stack.
+19. Push the value (FRAME_ 0 { z }) to the stack.
 20. Let [val]* be $eval_expr(expr_G)*.
-21. Pop the activation of _f from the stack.
-22. Push the activation of z to the stack.
+21. Pop the value (FRAME_ 0 { _f }) from the stack.
+22. Push the value (FRAME_ 0 { z }) to the stack.
 23. Let [ref]** be $eval_expr(expr_E)**.
-24. Pop the activation of _f from the stack.
+24. Pop the value (FRAME_ 0 { _f }) from the stack.
 25. Let moduleinst be $allocmodule(module, externaddr*, val*, ref**).
 26. Let f be { LOCALS: []; MODULE: moduleinst; }.
-27. Push the activation of f with arity 0 to the stack.
+27. Push the evaluation context (FRAME_ 0 { f }) to the stack.
 28. Execute the sequence (instr_E*).
 29. Execute the sequence (instr_D*).
 30. If (CALL x)? is defined, then:
   a. Execute the instruction (CALL x).
-31. Pop the activation of f with arity 0 from the stack.
+31. Pop the evaluation context (FRAME_ 0 { f }) from the stack.
 32. Return f.MODULE.
 
 invoke z fa val^n
 1. Let f be { LOCALS: []; MODULE: { TYPES: []; FUNCS: []; GLOBALS: []; TABLES: []; MEMS: []; ELEMS: []; DATAS: []; EXPORTS: []; }; }.
-2. Push the activation of f to the stack.
+2. Push the value (FRAME_ 0 { f }) to the stack.
 3. Let (t_1^n -> t_2*) be $funcinst(z)[fa].TYPE.
-4. Pop the activation of _f from the stack.
+4. Pop the value (FRAME_ 0 { _f }) from the stack.
 5. Let k be |t_2*|.
-6. Push the activation of f with arity k to the stack.
+6. Push the evaluation context (FRAME_ k { f }) to the stack.
 7. Push the values val^n to the stack.
 8. Execute the instruction (CALL_ADDR fa).
 9. Pop all values val* from the top of the stack.
-10. Pop the activation of f with arity k from the stack.
+10. Pop the evaluation context (FRAME_ k { f }) from the stack.
 11. Push the values val* to the stack.
 12. Pop the values val^k from the stack.
 13. Return val^k.
@@ -14557,11 +14482,13 @@ watsup 0.4 generator
 ......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+
+#. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Assert: Due to validation, a label is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{label}`.
 
-#. Pop the current label from the stack.
+#. Pop the current :math:`\mathsf{label}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -14570,17 +14497,9 @@ watsup 0.4 generator
 .....................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. If the top of the stack is a :math:`\mathsf{label}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+1. If the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   #. Let :math:`L` be the current label.
-
-   #. Let :math:`n` be the arity of :math:`L`.
-
-   #. Let :math:`{{\mathit{instr}'}^\ast}` be the continuation of :math:`L`.
+   a. Let :math:`({{\mathsf{label}}_{n}}{\{}~{{\mathit{instr}'}^\ast}~\})` be the current :math:`\mathsf{label}` context.
 
    #. If :math:`l` is :math:`0`, then:
 
@@ -14590,7 +14509,7 @@ watsup 0.4 generator
 
       #) Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-      #) Pop the current label from the stack.
+      #) Pop the current :math:`\mathsf{label}` context from the stack.
 
       #) Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -14602,19 +14521,17 @@ watsup 0.4 generator
 
       #) If :math:`l` is greater than :math:`0`, then:
 
-         a) Pop the current label from the stack.
+         a) Pop the current :math:`\mathsf{label}` context from the stack.
 
          #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
          #) Execute the instruction :math:`(\mathsf{br}~l - 1)`.
 
-#. Else if the top of the stack is a :math:`\mathsf{handler}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{handler}`, then:
 
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Exit from :math:`\mathsf{handler}`.
+   #. Pop the current :math:`\mathsf{handler}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -14717,9 +14634,7 @@ watsup 0.4 generator
 ......................
 
 
-1. Let :math:`f` be the current frame.
-
-#. Let :math:`n` be the arity of :math:`f`.
+1. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -14727,9 +14642,9 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{n}}` from the stack.
 
-#. Assert: Due to validation, a frame is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{frame}`.
 
-#. Pop the current frame from the stack.
+#. Pop the current :math:`\mathsf{frame}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -14738,15 +14653,9 @@ watsup 0.4 generator
 .......................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. If the top of the stack is a :math:`\mathsf{frame}`, then:
+1. If the first non-value entry of the stack is a :math:`\mathsf{frame}`, then:
 
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-   #. Let :math:`f` be the current frame.
-
-   #. Let :math:`n` be the arity of :math:`f`.
+   a. Let :math:`({{\mathsf{frame}}_{n}}{\{}~f~\})` be the current :math:`\mathsf{frame}` context.
 
    #. Assert: Due to validation, there are at least :math:`n` values on the top of the stack.
 
@@ -14754,17 +14663,15 @@ watsup 0.4 generator
 
    #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-   #. Pop the current frame from the stack.
+   #. Pop the current :math:`\mathsf{frame}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
-#. Else if the top of the stack is a :math:`\mathsf{label}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -14772,13 +14679,11 @@ watsup 0.4 generator
 
 #. Else:
 
-   a. If the top of the stack is a :math:`\mathsf{handler}`, then:
-
-      1) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+   a. If the first non-value entry of the stack is a :math:`\mathsf{handler}`, then:
 
-      #) Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+      1) Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-      #) Exit from :math:`\mathsf{handler}`.
+      #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
       #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -14789,11 +14694,13 @@ watsup 0.4 generator
 ........................
 
 
-1. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+
+#. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Assert: Due to validation, YetE: a handler is now on the top of the stack.
+#. Assert: Due to validation, the first non-value entry of the stack is a :math:`\mathsf{handler}`.
 
-#. Exit from :math:`\mathsf{handler}`.
+#. Pop the current :math:`\mathsf{handler}` context from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -15499,9 +15406,7 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{m}}` from the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast}`
@@ -15516,16 +15421,14 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{m}}` from the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is :math:`(\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast})`.
-
-#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{m}}{\{}~(\mathsf{loop}~{\mathit{bt}}~{{\mathit{instr}}^\ast})~\})`.
 
 
 :math:`\mathsf{br\_on\_cast}~l~{\mathit{rt}}_1~{\mathit{rt}}_2`
 ...............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, a value is on the top of the stack.
 
@@ -15548,7 +15451,7 @@ watsup 0.4 generator
 .....................................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, a value is on the top of the stack.
 
@@ -15626,13 +15529,9 @@ watsup 0.4 generator
 
       #) Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~{{\mathit{val}}^{n}}~{{{\mathrm{default}}}_{t}^\ast},\; \mathsf{module}~{\mathit{fi}}{.}\mathsf{module} \}\end{array}`.
 
-      #) Let :math:`F` be the activation of :math:`f` with arity :math:`m`.
-
-      #) Push :math:`F` to the stack.
-
-      #) Let :math:`L` be the label whose arity is :math:`m` and whose continuation is :math:`\epsilon`.
+      #) Push the value :math:`({{\mathsf{frame}}_{m}}{\{}~f~\})` to the stack.
 
-      #) Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`L`.
+      #) Enter :math:`{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{m}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{return\_call}~x`
@@ -15658,27 +15557,21 @@ watsup 0.4 generator
 
 1. Let :math:`z` be the current state.
 
-#. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-#. If the top of the stack is a :math:`\mathsf{label}`, then:
+#. If the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Pop the current label from the stack.
+   #. Pop the current :math:`\mathsf{label}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
    #. Execute the instruction :math:`(\mathsf{return\_call\_ref}~y)`.
 
-#. Else if the top of the stack is a :math:`\mathsf{handler}`, then:
-
-   a. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{handler}`, then:
 
-   #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
+   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-   #. Exit from :math:`\mathsf{handler}`.
+   #. Pop the current :math:`\mathsf{handler}` context from the stack.
 
    #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -15686,11 +15579,9 @@ watsup 0.4 generator
 
 #. Else:
 
-   a. If the top of the stack is a :math:`\mathsf{frame}`, then:
-
-      1) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+   a. If the first non-value entry of the stack is a :math:`\mathsf{frame}`, then:
 
-      #) Assert: Due to validation, a value is on the top of the stack.
+      1) Assert: Due to validation, a value is on the top of the stack.
 
       #) Pop the value :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` from the stack.
 
@@ -15698,7 +15589,7 @@ watsup 0.4 generator
 
       #) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}null}`, then:
 
-         a) Pop the current frame from the stack.
+         a) Pop the current :math:`\mathsf{frame}` context from the stack.
 
          #) Trap.
 
@@ -15720,7 +15611,7 @@ watsup 0.4 generator
 
             #. Pop all values :math:`{{\mathit{val}'}^\ast}` from the top of the stack.
 
-            #. Pop the current frame from the stack.
+            #. Pop the current :math:`\mathsf{frame}` context from the stack.
 
             #. Push the values :math:`{{\mathit{val}}^{n}}` to the stack.
 
@@ -15755,191 +15646,185 @@ watsup 0.4 generator
 
       #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-#. Else:
+#. Else if the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
-   a. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
-
-   #. If the top of the stack is a :math:`\mathsf{label}`, then:
-
-      1) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
-
-      #) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
+   a. If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
 
-         a) Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
+      1) Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
 
-         #) Pop the current label from the stack.
+      #) Pop the current :math:`\mathsf{label}` context from the stack.
 
-         #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+      #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-         #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+      #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-   #. Else if the top of the stack is a :math:`\mathsf{frame}`, then:
+#. Else:
 
-      1) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+   a. If the first non-value entry of the stack is a :math:`\mathsf{frame}`, then:
 
-      #) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
+      1) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
 
          a) Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
 
-         #) Pop the current frame from the stack.
+         #) Pop the current :math:`\mathsf{frame}` context from the stack.
 
          #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
          #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-   #. Else:
+   #. Else if not the first non-value entry of the stack is a :math:`\mathsf{handler}`, then:
 
-      1) If not the top of the stack is a :math:`\mathsf{handler}`, then:
+      1) Throw the exception :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` as a result.
 
-         a) Throw the exception :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` as a result.
+   #. Else:
 
-      #) Else:
+      1) Let :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}~\})` be the current :math:`\mathsf{handler}` context.
 
-         a) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+      #) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
 
-         #) Let :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}~\})` be the current context.
+         a) Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
 
-         #) If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
+         #) If :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}` is :math:`\epsilon`, then:
 
-            1. Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
+            1. Pop the current :math:`\mathsf{handler}` context from the stack.
 
-            #. If :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}` is :math:`\epsilon`, then:
+            #. Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-               a. Exit from :math:`\mathsf{handler}`.
+            #. Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-               #. Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+         #) Else if :math:`a` is greater than or equal to :math:`{|z{.}\mathsf{exns}|}`, then:
 
-               #. Execute the instruction :math:`\mathsf{throw\_ref}`.
+            1. Let :math:`{\mathit{catch}}_0~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-            #. Else if :math:`a` is greater than or equal to :math:`{|z{.}\mathsf{exns}|}`, then:
+            #. If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all}`, then:
 
-               a. Let :math:`{\mathit{catch}}_0~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+               a. Let :math:`(\mathsf{catch\_all}~l)` be :math:`{\mathit{catch}}_0`.
 
-               #. If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all}`, then:
+               #. Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  1) Let :math:`(\mathsf{catch\_all}~l)` be :math:`{\mathit{catch}}_0`.
+               #. Execute the instruction :math:`(\mathsf{br}~l)`.
 
-                  #) Exit from :math:`\mathsf{handler}`.
+            #. Else if :math:`{\mathit{catch}}_0` is not of the case :math:`\mathsf{catch\_all\_ref}`, then:
 
-                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
+               a. Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-               #. Else if :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all\_ref}`, then:
+               #. Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  1) Let :math:`(\mathsf{catch\_all\_ref}~l)` be :math:`{\mathit{catch}}_0`.
+               #. Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})` to the stack.
 
-                  #) Exit from :math:`\mathsf{handler}`.
+               #. Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+               #. Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
+            #. Else:
 
-               #. Else:
+               a. Let :math:`(\mathsf{catch\_all\_ref}~l)` be :math:`{\mathit{catch}}_0`.
 
-                  1) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+               #. Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  #) Exit from :math:`\mathsf{handler}`.
+               #. Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                  #) Let :math:`H` be :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})`.
+               #. Execute the instruction :math:`(\mathsf{br}~l)`.
 
-                  #) Push the handler :math:`H` to the stack.
+         #) Else:
 
-                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+            1. Let :math:`{{\mathit{val}}^\ast}` be :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{fields}`.
 
-                  #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+            #. Let :math:`{\mathit{catch}}_0~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-            #. Else:
+            #. If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch}`, then:
 
-               a. Let :math:`{{\mathit{val}}^\ast}` be :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{fields}`.
+               a. Let :math:`(\mathsf{catch}~x~l)` be :math:`{\mathit{catch}}_0`.
 
-               #. Let :math:`{\mathit{catch}}_0~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+               #. If :math:`x` is less than :math:`{|z{.}\mathsf{tags}|}` and :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{tag}` is :math:`z{.}\mathsf{tags}{}[x]`, then:
 
-               #. If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch}`, then:
+                  1) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  1) Let :math:`(\mathsf{catch}~x~l)` be :math:`{\mathit{catch}}_0`.
+                  #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
-                  #) If :math:`x` is less than :math:`{|z{.}\mathsf{tags}|}` and :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{tag}` is :math:`z{.}\mathsf{tags}{}[x]`, then:
+                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
 
-                     a) Exit from :math:`\mathsf{handler}`.
+               #. Else:
 
-                     #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+                  1) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-                     #) Execute the instruction :math:`(\mathsf{br}~l)`.
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  #) Else:
+                  #) Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})` to the stack.
 
-                     a) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                     #) Exit from :math:`\mathsf{handler}`.
+                  #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-                     #) Let :math:`H` be :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})`.
+            #. Else if :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_ref}`, then:
 
-                     #) Push the handler :math:`H` to the stack.
+               a. Let :math:`(\mathsf{catch\_ref}~x~l)` be :math:`{\mathit{catch}}_0`.
 
-                     #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+               #. If :math:`x` is greater than or equal to :math:`{|z{.}\mathsf{tags}|}`, then:
 
-                     #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+                  1) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-               #. Else if :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_ref}`, then:
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  1) Let :math:`(\mathsf{catch\_ref}~x~l)` be :math:`{\mathit{catch}}_0`.
+                  #) Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})` to the stack.
 
-                  #) If :math:`x` is less than :math:`{|z{.}\mathsf{tags}|}` and :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{tag}` is :math:`z{.}\mathsf{tags}{}[x]`, then:
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                     a) Exit from :math:`\mathsf{handler}`.
+                  #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-                     #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
+               #. Else if :math:`z{.}\mathsf{exns}{}[a]{.}\mathsf{tag}` is not :math:`z{.}\mathsf{tags}{}[x]`, then:
 
-                     #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+                  1) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-                     #) Execute the instruction :math:`(\mathsf{br}~l)`.
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  #) Else:
+                  #) Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})` to the stack.
 
-                     a) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                     #) Exit from :math:`\mathsf{handler}`.
+                  #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-                     #) Let :math:`H` be :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})`.
+               #. Else:
 
-                     #) Push the handler :math:`H` to the stack.
+                  1) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                     #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+                  #) Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
-                     #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-               #. Else:
+                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
 
-                  1) If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all}`, then:
+            #. Else:
 
-                     a) Let :math:`(\mathsf{catch\_all}~l)` be :math:`{\mathit{catch}}_0`.
+               a. If :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all}`, then:
 
-                     #) Exit from :math:`\mathsf{handler}`.
+                  1) Let :math:`(\mathsf{catch\_all}~l)` be :math:`{\mathit{catch}}_0`.
 
-                     #) Execute the instruction :math:`(\mathsf{br}~l)`.
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                  #) Else if :math:`{\mathit{catch}}_0` is of the case :math:`\mathsf{catch\_all\_ref}`, then:
+                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
 
-                     a) Let :math:`(\mathsf{catch\_all\_ref}~l)` be :math:`{\mathit{catch}}_0`.
+               #. Else if :math:`{\mathit{catch}}_0` is not of the case :math:`\mathsf{catch\_all\_ref}`, then:
 
-                     #) Exit from :math:`\mathsf{handler}`.
+                  1) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
 
-                     #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                     #) Execute the instruction :math:`(\mathsf{br}~l)`.
+                  #) Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})` to the stack.
 
-                  #) Else:
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                     a) Let :math:`{\mathit{catch}}~{{\mathit{catch}'}^\ast}` be :math:`{{\mathit{catch}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}`.
+                  #) Execute the instruction :math:`\mathsf{throw\_ref}`.
 
-                     #) Exit from :math:`\mathsf{handler}`.
+               #. Else:
 
-                     #) Let :math:`H` be :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}'}^\ast}~\})`.
+                  1) Let :math:`(\mathsf{catch\_all\_ref}~l)` be :math:`{\mathit{catch}}_0`.
 
-                     #) Push the handler :math:`H` to the stack.
+                  #) Pop the current :math:`\mathsf{handler}` context from the stack.
 
-                     #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
+                  #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-                     #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+                  #) Execute the instruction :math:`(\mathsf{br}~l)`.
 
 
 :math:`\mathsf{try\_table}~{\mathit{bt}}~{{\mathit{catch}}^\ast}~{{\mathit{instr}}^\ast}`
@@ -15954,13 +15839,9 @@ watsup 0.4 generator
 
 #. Pop the values :math:`{{\mathit{val}}^{m}}` from the stack.
 
-#. Let :math:`H` be :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}^\ast}~\})`.
-
-#. Push the handler :math:`H` to the stack.
+#. Push the value :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}^\ast}~\})` to the stack.
 
-#. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is :math:`\epsilon`.
-
-#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`L`.
+#. Enter :math:`{{\mathit{val}}^{m}}~{{\mathit{instr}}^\ast}` with label :math:`({{\mathsf{label}}_{n}}{\{}~\epsilon~\})`.
 
 
 :math:`\mathsf{ref{.}null}~x`
@@ -15987,7 +15868,7 @@ watsup 0.4 generator
 .........................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, a value is on the top of the stack.
 
@@ -16008,7 +15889,7 @@ watsup 0.4 generator
 .........................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Assert: Due to validation, a value is on the top of the stack.
 
@@ -21498,7 +21379,7 @@ watsup 0.4 generator
 ........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f`.
 
@@ -21507,7 +21388,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{tags}`.
 
@@ -21516,7 +21397,7 @@ watsup 0.4 generator
 .............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -21595,7 +21476,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{module}{.}\mathsf{types}{}[x]`.
 
@@ -21604,7 +21485,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{funcs}{}[f{.}\mathsf{module}{.}\mathsf{funcs}{}[x]]`.
 
@@ -21613,7 +21494,7 @@ watsup 0.4 generator
 ............................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]`.
 
@@ -21622,7 +21503,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]`.
 
@@ -21631,7 +21512,7 @@ watsup 0.4 generator
 .........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]`.
 
@@ -21640,7 +21521,7 @@ watsup 0.4 generator
 .........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{tags}{}[f{.}\mathsf{module}{.}\mathsf{tags}{}[x]]`.
 
@@ -21649,7 +21530,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{elems}{}[f{.}\mathsf{module}{.}\mathsf{elems}{}[x]]`.
 
@@ -21658,7 +21539,7 @@ watsup 0.4 generator
 ..........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`s{.}\mathsf{datas}{}[f{.}\mathsf{module}{.}\mathsf{datas}{}[x]]`.
 
@@ -21667,7 +21548,7 @@ watsup 0.4 generator
 ...........................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Return :math:`f{.}\mathsf{locals}{}[x]`.
 
@@ -21676,7 +21557,7 @@ watsup 0.4 generator
 ..............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`f{.}\mathsf{locals}{}[x]` with :math:`v`.
 
@@ -21685,7 +21566,7 @@ watsup 0.4 generator
 ...............................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{globals}{}[f{.}\mathsf{module}{.}\mathsf{globals}{}[x]]{.}\mathsf{value}` with :math:`v`.
 
@@ -21694,7 +21575,7 @@ watsup 0.4 generator
 .................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]{.}\mathsf{refs}{}[i]` with :math:`r`.
 
@@ -21703,7 +21584,7 @@ watsup 0.4 generator
 ..............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{tables}{}[f{.}\mathsf{module}{.}\mathsf{tables}{}[x]]` with :math:`{\mathit{ti}}`.
 
@@ -21712,7 +21593,7 @@ watsup 0.4 generator
 .........................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]{.}\mathsf{bytes}{}[i : j]` with :math:`{b^\ast}`.
 
@@ -21721,7 +21602,7 @@ watsup 0.4 generator
 ............................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{mems}{}[f{.}\mathsf{module}{.}\mathsf{mems}{}[x]]` with :math:`{\mathit{mi}}`.
 
@@ -21730,7 +21611,7 @@ watsup 0.4 generator
 ....................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{elems}{}[f{.}\mathsf{module}{.}\mathsf{elems}{}[x]]{.}\mathsf{refs}` with :math:`{r^\ast}`.
 
@@ -21739,7 +21620,7 @@ watsup 0.4 generator
 ....................................................
 
 
-1. Let :math:`f` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. Replace :math:`s{.}\mathsf{datas}{}[f{.}\mathsf{module}{.}\mathsf{datas}{}[x]]{.}\mathsf{bytes}` with :math:`{b^\ast}`.
 
@@ -22280,7 +22161,7 @@ watsup 0.4 generator
 .................................................................................................................................................................................
 
 
-1. Let :math:`z` be the current frame.
+1. Let :math:`({{\mathsf{frame}}_{}}{\{})` be the current :math:`\mathsf{frame}` context.
 
 #. If :math:`{{\mathit{globaltype}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}` is :math:`\epsilon` and :math:`{{\mathit{expr}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}` is :math:`\epsilon`, then:
 
@@ -22347,29 +22228,29 @@ watsup 0.4 generator
 
 #. Let :math:`z` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~\epsilon,\; \mathsf{module}~{\mathit{moduleinst}}_0 \}\end{array}`.
 
-#. Push the activation of :math:`z` to the stack.
+#. Push the value :math:`({{\mathsf{frame}}_{0}}{\{})` to the stack.
 
 #. Let :math:`{{\mathit{val}}_{\mathsf{g}}^\ast}` be :math:`{{{\mathrm{evalglobal}}^\ast}}{(z, {{\mathit{globaltype}}^\ast}, {{\mathit{expr}}_{\mathsf{g}}^\ast})}`.
 
-#. Pop the activation of :math:`{z'}` from the stack.
+#. Pop the value :math:`({{\mathsf{frame}}_{0}}{\{})` from the stack.
 
-#. Push the activation of :math:`{z'}` to the stack.
+#. Push the value :math:`({{\mathsf{frame}}_{0}}{\{})` to the stack.
 
 #. Let :math:`{{\mathit{ref}}_{\mathsf{t}}^\ast}` be :math:`{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{t}})^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({{\mathsf{frame}}_{0}}{\{})` from the stack.
 
-#. Push the activation of :math:`{z'}` to the stack.
+#. Push the value :math:`({{\mathsf{frame}}_{0}}{\{})` to the stack.
 
 #. Let :math:`{{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast}` be :math:`{{{\mathrm{eval}}_{\mathit{expr}}({\mathit{expr}}_{\mathsf{e}})^\ast}^\ast}`.
 
-#. Pop the activation of :math:`f` from the stack.
+#. Pop the value :math:`({{\mathsf{frame}}_{0}}{\{})` from the stack.
 
 #. Let :math:`{\mathit{moduleinst}}` be :math:`{\mathrm{allocmodule}}({\mathit{module}}, {{\mathit{externaddr}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {{{\mathit{ref}}_{\mathsf{e}}^\ast}^\ast})`.
 
 #. Let :math:`f` be :math:`\{ \begin{array}[t]{@{}l@{}}\mathsf{locals}~\epsilon,\; \mathsf{module}~{\mathit{moduleinst}} \}\end{array}`.
 
-#. Push the activation of :math:`f` with arity :math:`0` to the stack.
+#. Push the evaluation context :math:`({{\mathsf{frame}}_{0}}{\{})` to the stack.
 
 #. Execute the sequence :math:`{{\mathit{instr}}_{\mathsf{e}}^\ast}`.
 
@@ -22379,7 +22260,7 @@ watsup 0.4 generator
 
    a. Execute the instruction :math:`{\mathit{instr}}_{\mathsf{s}}`.
 
-#. Pop the activation of :math:`f` with arity :math:`0` from the stack.
+#. Pop the evaluation context :math:`({{\mathsf{frame}}_{0}}{\{})` from the stack.
 
 #. Return :math:`f{.}\mathsf{module}`.
 
@@ -22400,7 +22281,7 @@ watsup 0.4 generator
 
 #. Let :math:`k` be :math:`{|{t_2^\ast}|}`.
 
-#. Push the activation of :math:`f` with arity :math:`k` to the stack.
+#. Push the evaluation context :math:`({{\mathsf{frame}}_{k}}{\{})` to the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -22410,7 +22291,7 @@ watsup 0.4 generator
 
 #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. Pop the activation of :math:`f` with arity :math:`k` from the stack.
+#. Pop the evaluation context :math:`({{\mathsf{frame}}_{k}}{\{})` from the stack.
 
 #. Push the values :math:`{{\mathit{val}}^\ast}` to the stack.
 
@@ -23804,37 +23685,33 @@ Step_pure/if bt instr_1* instr_2*
   a. Execute the instruction (BLOCK bt instr_2*).
 
 Step_pure/label
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, a label is now on the top of the stack.
-3. Pop the current label from the stack.
-4. Push the values val* to the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+2. Pop all values val* from the top of the stack.
+3. Assert: Due to validation, the first non-value entry of the stack is a LABEL_.
+4. Pop the current LABEL_ context from the stack.
+5. Push the values val* to the stack.
 
 Step_pure/br l
-1. Pop all values val* from the top of the stack.
-2. If the top of the stack is a LABEL_, then:
-  a. Push the values val* to the stack.
-  b. Let L be the current label.
-  c. Let n be the arity of L.
-  d. Let instr'* be the continuation of L.
-  e. If (l is 0), then:
+1. If the first non-value entry of the stack is a LABEL_, then:
+  a. Let (LABEL_ n { instr'* }) be the current LABEL_ context.
+  b. If (l is 0), then:
     1) Assert: Due to validation, there are at least n values on the top of the stack.
     2) Pop the values val^n from the stack.
     3) Pop all values val'* from the top of the stack.
-    4) Pop the current label from the stack.
+    4) Pop the current LABEL_ context from the stack.
     5) Push the values val^n to the stack.
     6) Execute the instruction instr'*.
-  f. Else:
+  c. Else:
     1) Pop all values val* from the top of the stack.
     2) If (l > 0), then:
-      a) Pop the current label from the stack.
+      a) Pop the current LABEL_ context from the stack.
       b) Push the values val* to the stack.
       c) Execute the instruction (BR (l - 1)).
-3. Else if the top of the stack is a HANDLER_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Exit from HANDLER_.
-  d. Push the values val* to the stack.
-  e. Execute the instruction (BR l).
+2. Else if the first non-value entry of the stack is a HANDLER_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current HANDLER_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction (BR l).
 
 Step_pure/br_if l
 1. Assert: Due to validation, a value of value type I32 is on the top of the stack.
@@ -23880,44 +23757,39 @@ Step_pure/return_call_indirect x yy
 3. Execute the instruction (RETURN_CALL_REF yy).
 
 Step_pure/frame
-1. Let f be the current frame.
-2. Let n be the arity of f.
+1. Let (FRAME_ n { f }) be the current FRAME_ context.
+2. Assert: Due to validation, there are at least n values on the top of the stack.
 3. Assert: Due to validation, there are at least n values on the top of the stack.
-4. Assert: Due to validation, there are at least n values on the top of the stack.
-5. Pop the values val^n from the stack.
-6. Assert: Due to validation, a frame is now on the top of the stack.
-7. Pop the current frame from the stack.
-8. Push the values val^n to the stack.
+4. Pop the values val^n from the stack.
+5. Assert: Due to validation, the first non-value entry of the stack is a FRAME_.
+6. Pop the current FRAME_ context from the stack.
+7. Push the values val^n to the stack.
 
 Step_pure/return
-1. Pop all values val* from the top of the stack.
-2. If the top of the stack is a FRAME_, then:
-  a. Push the values val* to the stack.
-  b. Let f be the current frame.
-  c. Let n be the arity of f.
-  d. Assert: Due to validation, there are at least n values on the top of the stack.
-  e. Pop the values val^n from the stack.
-  f. Pop all values val'* from the top of the stack.
-  g. Pop the current frame from the stack.
-  h. Push the values val^n to the stack.
-3. Else if the top of the stack is a LABEL_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Pop the current label from the stack.
-  d. Push the values val* to the stack.
-  e. Execute the instruction RETURN.
-4. Else if the top of the stack is a HANDLER_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Exit from HANDLER_.
-  d. Push the values val* to the stack.
-  e. Execute the instruction RETURN.
+1. If the first non-value entry of the stack is a FRAME_, then:
+  a. Let (FRAME_ n { f }) be the current FRAME_ context.
+  b. Assert: Due to validation, there are at least n values on the top of the stack.
+  c. Pop the values val^n from the stack.
+  d. Pop all values val'* from the top of the stack.
+  e. Pop the current FRAME_ context from the stack.
+  f. Push the values val^n to the stack.
+2. Else if the first non-value entry of the stack is a LABEL_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current LABEL_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction RETURN.
+3. Else if the first non-value entry of the stack is a HANDLER_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current HANDLER_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction RETURN.
 
 Step_pure/handler
-1. Pop all values val* from the top of the stack.
-2. Assert: Due to validation, YetE (a handler is now on the top of the stack).
-3. Exit from HANDLER_.
-4. Push the values val* to the stack.
+1. Assert: Due to validation, a value is on the top of the stack.
+2. Pop all values val* from the top of the stack.
+3. Assert: Due to validation, the first non-value entry of the stack is a HANDLER_.
+4. Pop the current HANDLER_ context from the stack.
+5. Push the values val* to the stack.
 
 Step_pure/unop nt unop
 1. Assert: Due to validation, a value of value type numtype_0 is on the top of the stack.
@@ -24252,19 +24124,17 @@ Step_read/block bt instr*
 2. Let (t_1^m -> t_2^n) be $blocktype_(z, bt).
 3. Assert: Due to validation, there are at least m values on the top of the stack.
 4. Pop the values val^m from the stack.
-5. Let L be the label_n{[]}.
-6. Enter val^m :: instr* with label L.
+5. Enter val^m :: instr* with label (LABEL_ n { [] }).
 
 Step_read/loop bt instr*
 1. Let z be the current state.
 2. Let (t_1^m -> t_2^n) be $blocktype_(z, bt).
 3. Assert: Due to validation, there are at least m values on the top of the stack.
 4. Pop the values val^m from the stack.
-5. Let L be the label_m{[(LOOP bt instr*)]}.
-6. Enter val^m :: instr* with label L.
+5. Enter val^m :: instr* with label (LABEL_ m { [(LOOP bt instr*)] }).
 
 Step_read/br_on_cast l rt_1 rt_2
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Assert: Due to validation, a value is on the top of the stack.
 3. Pop the value ref from the stack.
 4. Let rt be $Ref_type(ref).
@@ -24275,7 +24145,7 @@ Step_read/br_on_cast l rt_1 rt_2
   a. Execute the instruction (BR l).
 
 Step_read/br_on_cast_fail l rt_1 rt_2
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Assert: Due to validation, a value is on the top of the stack.
 3. Pop the value ref from the stack.
 4. Let rt be $Ref_type(ref).
@@ -24313,10 +24183,8 @@ Step_read/call_ref yy
     9) Assert: Due to validation, there are at least n values on the top of the stack.
     10) Pop the values val^n from the stack.
     11) Let f be { LOCALS: ?(val)^n :: $default_(t)*; MODULE: fi.MODULE; }.
-    12) Let F be the activation of f with arity m.
-    13) Push F to the stack.
-    14) Let L be the label_m{[]}.
-    15) Enter instr* with label L.
+    12) Push the value (FRAME_ m { f }) to the stack.
+    13) Enter instr* with label (LABEL_ m { [] }).
 
 Step_read/return_call x
 1. Let z be the current state.
@@ -24328,28 +24196,24 @@ Step_read/return_call x
 
 Step_read/return_call_ref yy
 1. Let z be the current state.
-2. Pop all values val* from the top of the stack.
-3. If the top of the stack is a LABEL_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Pop the current label from the stack.
-  d. Push the values val* to the stack.
-  e. Execute the instruction (RETURN_CALL_REF yy).
-4. Else if the top of the stack is a HANDLER_, then:
-  a. Push the values val* to the stack.
-  b. Pop all values val* from the top of the stack.
-  c. Exit from HANDLER_.
-  d. Push the values val* to the stack.
-  e. Execute the instruction (RETURN_CALL_REF yy).
-5. Else if the top of the stack is a FRAME_, then:
-  a. Push the values val* to the stack.
-  b. Assert: Due to validation, a value is on the top of the stack.
-  c. Pop the value instr_u0 from the stack.
-  d. Pop all values val* from the top of the stack.
-  e. If instr_u0 is of the case REF.NULL, then:
-    1) Pop the current frame from the stack.
+2. If the first non-value entry of the stack is a LABEL_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current LABEL_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction (RETURN_CALL_REF yy).
+3. Else if the first non-value entry of the stack is a HANDLER_, then:
+  a. Pop all values val* from the top of the stack.
+  b. Pop the current HANDLER_ context from the stack.
+  c. Push the values val* to the stack.
+  d. Execute the instruction (RETURN_CALL_REF yy).
+4. Else if the first non-value entry of the stack is a FRAME_, then:
+  a. Assert: Due to validation, a value is on the top of the stack.
+  b. Pop the value instr_u0 from the stack.
+  c. Pop all values val* from the top of the stack.
+  d. If instr_u0 is of the case REF.NULL, then:
+    1) Pop the current FRAME_ context from the stack.
     2) Trap.
-  f. If instr_u0 is of the case REF.FUNC_ADDR, then:
+  e. If instr_u0 is of the case REF.FUNC_ADDR, then:
     1) Let (REF.FUNC_ADDR a) be instr_u0.
     2) If (a < |$funcinst(z)|), then:
       a) Assert: Due to validation, $expanddt($funcinst(z)[a].TYPE) is of the case FUNC.
@@ -24358,7 +24222,7 @@ Step_read/return_call_ref yy
       d) Assert: Due to validation, there are at least n values on the top of the stack.
       e) Pop the values val^n from the stack.
       f) Pop all values val'* from the top of the stack.
-      g) Pop the current frame from the stack.
+      g) Pop the current FRAME_ context from the stack.
       h) Push the values val^n to the stack.
       i) Push the value (REF.FUNC_ADDR a) to the stack.
       j) Execute the instruction (CALL_REF yy).
@@ -24375,107 +24239,102 @@ Step_read/throw_ref
     1) Let (REF.EXN_ADDR a) be instr_u0.
     2) Push the value (REF.EXN_ADDR a) to the stack.
     3) Execute the instruction THROW_REF.
-7. Else:
-  a. Pop all values val* from the top of the stack.
-  b. If the top of the stack is a LABEL_, then:
-    1) Push the values val* to the stack.
-    2) If instr_u0 is of the case REF.EXN_ADDR, then:
-      a) Let (REF.EXN_ADDR a) be instr_u0.
-      b) Pop the current label from the stack.
-      c) Push the value (REF.EXN_ADDR a) to the stack.
-      d) Execute the instruction THROW_REF.
-  c. Else if the top of the stack is a FRAME_, then:
-    1) Push the values val* to the stack.
-    2) If instr_u0 is of the case REF.EXN_ADDR, then:
-      a) Let (REF.EXN_ADDR a) be instr_u0.
-      b) Pop the current frame from the stack.
-      c) Push the value (REF.EXN_ADDR a) to the stack.
-      d) Execute the instruction THROW_REF.
-  d. Else if not the top of the stack is a HANDLER_, then:
-    1) Throw the exception instr_u0 as a result.
-  e. Else:
-    1) Push the values val* to the stack.
-    2) Let (HANDLER_ n { catch_u1* }) be the current context.
-    3) If instr_u0 is of the case REF.EXN_ADDR, then:
-      a) Let (REF.EXN_ADDR a) be instr_u0.
-      b) If (catch_u1* is []), then:
-        1. Exit from HANDLER_.
-        2. Push the value (REF.EXN_ADDR a) to the stack.
-        3. Execute the instruction THROW_REF.
-      c) Else if (a ≥ |$exninst(z)|), then:
-        1. Let [catch_0] :: catch'* be catch_u1*.
-        2. If catch_0 is of the case CATCH_ALL, then:
-          a. Let (CATCH_ALL l) be catch_0.
-          b. Exit from HANDLER_.
-          c. Execute the instruction (BR l).
-        3. Else if catch_0 is of the case CATCH_ALL_REF, then:
-          a. Let (CATCH_ALL_REF l) be catch_0.
-          b. Exit from HANDLER_.
-          c. Push the value (REF.EXN_ADDR a) to the stack.
-          d. Execute the instruction (BR l).
-        4. Else:
-          a. Let [catch] :: catch'* be catch_u1*.
-          b. Exit from HANDLER_.
-          c. Let H be (HANDLER_ n { catch'* }).
-          d. Push the handler H to the stack.
-          e. Push the value (REF.EXN_ADDR a) to the stack.
-          f. Execute the instruction THROW_REF.
+7. Else if the first non-value entry of the stack is a LABEL_, then:
+  a. If instr_u0 is of the case REF.EXN_ADDR, then:
+    1) Let (REF.EXN_ADDR a) be instr_u0.
+    2) Pop the current LABEL_ context from the stack.
+    3) Push the value (REF.EXN_ADDR a) to the stack.
+    4) Execute the instruction THROW_REF.
+8. Else if the first non-value entry of the stack is a FRAME_, then:
+  a. If instr_u0 is of the case REF.EXN_ADDR, then:
+    1) Let (REF.EXN_ADDR a) be instr_u0.
+    2) Pop the current FRAME_ context from the stack.
+    3) Push the value (REF.EXN_ADDR a) to the stack.
+    4) Execute the instruction THROW_REF.
+9. Else if not the first non-value entry of the stack is a HANDLER_, then:
+  a. Throw the exception instr_u0 as a result.
+10. Else:
+  a. Let (HANDLER_ n { catch_u1* }) be the current HANDLER_ context.
+  b. If instr_u0 is of the case REF.EXN_ADDR, then:
+    1) Let (REF.EXN_ADDR a) be instr_u0.
+    2) If (catch_u1* is []), then:
+      a) Pop the current HANDLER_ context from the stack.
+      b) Push the value (REF.EXN_ADDR a) to the stack.
+      c) Execute the instruction THROW_REF.
+    3) Else if (a ≥ |$exninst(z)|), then:
+      a) Let [catch_0] :: catch'* be catch_u1*.
+      b) If catch_0 is of the case CATCH_ALL, then:
+        1. Let (CATCH_ALL l) be catch_0.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Execute the instruction (BR l).
+      c) Else if catch_0 is not of the case CATCH_ALL_REF, then:
+        1. Let [catch] :: catch'* be catch_u1*.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Push the value (HANDLER_ n { catch'* }) to the stack.
+        4. Push the value (REF.EXN_ADDR a) to the stack.
+        5. Execute the instruction THROW_REF.
       d) Else:
-        1. Let val* be $exninst(z)[a].FIELDS.
-        2. Let [catch_0] :: catch'* be catch_u1*.
-        3. If catch_0 is of the case CATCH, then:
-          a. Let (CATCH x l) be catch_0.
-          b. If ((x < |$tagaddr(z)|) and ($exninst(z)[a].TAG is $tagaddr(z)[x])), then:
-            1) Exit from HANDLER_.
-            2) Push the values val* to the stack.
-            3) Execute the instruction (BR l).
-          c. Else:
-            1) Let [catch] :: catch'* be catch_u1*.
-            2) Exit from HANDLER_.
-            3) Let H be (HANDLER_ n { catch'* }).
-            4) Push the handler H to the stack.
-            5) Push the value (REF.EXN_ADDR a) to the stack.
-            6) Execute the instruction THROW_REF.
-        4. Else if catch_0 is of the case CATCH_REF, then:
-          a. Let (CATCH_REF x l) be catch_0.
-          b. If ((x < |$tagaddr(z)|) and ($exninst(z)[a].TAG is $tagaddr(z)[x])), then:
-            1) Exit from HANDLER_.
-            2) Push the values val* to the stack.
-            3) Push the value (REF.EXN_ADDR a) to the stack.
-            4) Execute the instruction (BR l).
-          c. Else:
-            1) Let [catch] :: catch'* be catch_u1*.
-            2) Exit from HANDLER_.
-            3) Let H be (HANDLER_ n { catch'* }).
-            4) Push the handler H to the stack.
-            5) Push the value (REF.EXN_ADDR a) to the stack.
-            6) Execute the instruction THROW_REF.
-        5. Else if catch_0 is of the case CATCH_ALL, then:
-          a. Let (CATCH_ALL l) be catch_0.
-          b. Exit from HANDLER_.
+        1. Let (CATCH_ALL_REF l) be catch_0.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Push the value (REF.EXN_ADDR a) to the stack.
+        4. Execute the instruction (BR l).
+    4) Else:
+      a) Let val* be $exninst(z)[a].FIELDS.
+      b) Let [catch_0] :: catch'* be catch_u1*.
+      c) If catch_0 is of the case CATCH, then:
+        1. Let (CATCH x l) be catch_0.
+        2. If ((x < |$tagaddr(z)|) and ($exninst(z)[a].TAG is $tagaddr(z)[x])), then:
+          a. Pop the current HANDLER_ context from the stack.
+          b. Push the values val* to the stack.
           c. Execute the instruction (BR l).
-        6. Else if catch_0 is of the case CATCH_ALL_REF, then:
-          a. Let (CATCH_ALL_REF l) be catch_0.
-          b. Exit from HANDLER_.
+        3. Else:
+          a. Let [catch] :: catch'* be catch_u1*.
+          b. Pop the current HANDLER_ context from the stack.
+          c. Push the value (HANDLER_ n { catch'* }) to the stack.
+          d. Push the value (REF.EXN_ADDR a) to the stack.
+          e. Execute the instruction THROW_REF.
+      d) Else if catch_0 is of the case CATCH_REF, then:
+        1. Let (CATCH_REF x l) be catch_0.
+        2. If (x ≥ |$tagaddr(z)|), then:
+          a. Let [catch] :: catch'* be catch_u1*.
+          b. Pop the current HANDLER_ context from the stack.
+          c. Push the value (HANDLER_ n { catch'* }) to the stack.
+          d. Push the value (REF.EXN_ADDR a) to the stack.
+          e. Execute the instruction THROW_REF.
+        3. Else if ($exninst(z)[a].TAG is not $tagaddr(z)[x]), then:
+          a. Let [catch] :: catch'* be catch_u1*.
+          b. Pop the current HANDLER_ context from the stack.
+          c. Push the value (HANDLER_ n { catch'* }) to the stack.
+          d. Push the value (REF.EXN_ADDR a) to the stack.
+          e. Execute the instruction THROW_REF.
+        4. Else:
+          a. Pop the current HANDLER_ context from the stack.
+          b. Push the values val* to the stack.
           c. Push the value (REF.EXN_ADDR a) to the stack.
           d. Execute the instruction (BR l).
-        7. Else:
-          a. Let [catch] :: catch'* be catch_u1*.
-          b. Exit from HANDLER_.
-          c. Let H be (HANDLER_ n { catch'* }).
-          d. Push the handler H to the stack.
-          e. Push the value (REF.EXN_ADDR a) to the stack.
-          f. Execute the instruction THROW_REF.
+      e) Else if catch_0 is of the case CATCH_ALL, then:
+        1. Let (CATCH_ALL l) be catch_0.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Execute the instruction (BR l).
+      f) Else if catch_0 is not of the case CATCH_ALL_REF, then:
+        1. Let [catch] :: catch'* be catch_u1*.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Push the value (HANDLER_ n { catch'* }) to the stack.
+        4. Push the value (REF.EXN_ADDR a) to the stack.
+        5. Execute the instruction THROW_REF.
+      g) Else:
+        1. Let (CATCH_ALL_REF l) be catch_0.
+        2. Pop the current HANDLER_ context from the stack.
+        3. Push the value (REF.EXN_ADDR a) to the stack.
+        4. Execute the instruction (BR l).
 
 Step_read/try_table bt catch* instr*
 1. Let z be the current state.
 2. Let (t_1^m -> t_2^n) be $blocktype_(z, bt).
 3. Assert: Due to validation, there are at least m values on the top of the stack.
 4. Pop the values val^m from the stack.
-5. Let H be (HANDLER_ n { catch* }).
-6. Push the handler H to the stack.
-7. Let L be the label_n{[]}.
-8. Enter val^m :: instr* with label L.
+5. Push the value (HANDLER_ n { catch* }) to the stack.
+6. Enter val^m :: instr* with label (LABEL_ n { [] }).
 
 Step_read/ref.null $idx(x)
 1. Let z be the current state.
@@ -24487,7 +24346,7 @@ Step_read/ref.func x
 3. Push the value (REF.FUNC_ADDR $moduleinst(z).FUNCS[x]) to the stack.
 
 Step_read/ref.test rt
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Assert: Due to validation, a value is on the top of the stack.
 3. Pop the value ref from the stack.
 4. Let rt' be $Ref_type(ref).
@@ -24497,7 +24356,7 @@ Step_read/ref.test rt
   a. Push the value (I32.CONST 0) to the stack.
 
 Step_read/ref.cast rt
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Assert: Due to validation, a value is on the top of the stack.
 3. Pop the value ref from the stack.
 4. Let rt' be $Ref_type(ref).
@@ -27121,15 +26980,15 @@ store
 1. Return.
 
 frame
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.
 
 tagaddr
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.TAGS.
 
 moduleinst
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.
 
 funcinst
@@ -27163,71 +27022,71 @@ exninst
 1. Return s.EXNS.
 
 type x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.MODULE.TYPES[x].
 
 func x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.FUNCS[f.MODULE.FUNCS[x]].
 
 global x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.GLOBALS[f.MODULE.GLOBALS[x]].
 
 table x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.TABLES[f.MODULE.TABLES[x]].
 
 mem x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.MEMS[f.MODULE.MEMS[x]].
 
 tag x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.TAGS[f.MODULE.TAGS[x]].
 
 elem x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.ELEMS[f.MODULE.ELEMS[x]].
 
 data x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return s.DATAS[f.MODULE.DATAS[x]].
 
 local x
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Return f.LOCALS[x].
 
 with_local x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace f.LOCALS[x] with ?(v).
 
 with_global x v
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.GLOBALS[f.MODULE.GLOBALS[x]].VALUE with v.
 
 with_table x i r
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]].REFS[i] with r.
 
 with_tableinst x ti
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.TABLES[f.MODULE.TABLES[x]] with ti.
 
 with_mem x i j b*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] with b*.
 
 with_meminst x mi
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.MEMS[f.MODULE.MEMS[x]] with mi.
 
 with_elem x r*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.ELEMS[f.MODULE.ELEMS[x]].REFS with r*.
 
 with_data x b*
-1. Let f be the current frame.
+1. Let (FRAME_ _ { f }) be the current FRAME_ context.
 2. Replace s.DATAS[f.MODULE.DATAS[x]].BYTES with b*.
 
 with_struct a i fv
@@ -27483,7 +27342,7 @@ rundata_ x (DATA b^n datamode_u0)
 4. Return instr* :: [(I32.CONST 0), (I32.CONST n), (MEMORY.INIT y x), (DATA.DROP x)].
 
 evalglobals z globaltype_u0* expr_u1*
-1. Let z be the current frame.
+1. Let (FRAME_ _ { z }) be the current FRAME_ context.
 2. If ((globaltype_u0* is []) and (expr_u1* is [])), then:
   a. Return [].
 3. Assert: Due to validation, (|expr_u1*| ≥ 1).
@@ -27516,23 +27375,23 @@ instantiate z module externaddr*
 16. Let (ELEM reftype expr_E* elemmode)* be elem*.
 17. Let instr_S? be (CALL x)?.
 18. Let z be { LOCALS: []; MODULE: moduleinst_0; }.
-19. Push the activation of z to the stack.
+19. Push the value (FRAME_ 0 { z }) to the stack.
 20. Let val_G* be $evalglobals(z, globaltype*, expr_G*).
-21. Pop the activation of z' from the stack.
-22. Push the activation of z' to the stack.
+21. Pop the value (FRAME_ 0 { z' }) from the stack.
+22. Push the value (FRAME_ 0 { z' }) to the stack.
 23. Let [ref_T]* be $eval_expr(expr_T)*.
-24. Pop the activation of _f from the stack.
-25. Push the activation of z' to the stack.
+24. Pop the value (FRAME_ 0 { _f }) from the stack.
+25. Push the value (FRAME_ 0 { z' }) to the stack.
 26. Let [ref_E]** be $eval_expr(expr_E)**.
-27. Pop the activation of _f from the stack.
+27. Pop the value (FRAME_ 0 { _f }) from the stack.
 28. Let moduleinst be $allocmodule(module, externaddr*, val_G*, ref_T*, ref_E**).
 29. Let f be { LOCALS: []; MODULE: moduleinst; }.
-30. Push the activation of f with arity 0 to the stack.
+30. Push the evaluation context (FRAME_ 0 { f }) to the stack.
 31. Execute the sequence (instr_E*).
 32. Execute the sequence (instr_D*).
 33. If instr_S? is defined, then:
   a. Execute the instruction instr_S.
-34. Pop the activation of f with arity 0 from the stack.
+34. Pop the evaluation context (FRAME_ 0 { f }) from the stack.
 35. Return f.MODULE.
 
 invoke funcaddr val*
@@ -27542,12 +27401,12 @@ invoke funcaddr val*
 4. Let (t_1* -> t_2*) be functype_0.
 5. Assert: Due to validation, ($Val_type(val) is t_1)*.
 6. Let k be |t_2*|.
-7. Push the activation of f with arity k to the stack.
+7. Push the evaluation context (FRAME_ k { f }) to the stack.
 8. Push the values val* to the stack.
 9. Push the value (REF.FUNC_ADDR funcaddr) to the stack.
 10. Execute the instruction (CALL_REF s.FUNCS[funcaddr].TYPE).
 11. Pop all values val* from the top of the stack.
-12. Pop the activation of f with arity k from the stack.
+12. Pop the evaluation context (FRAME_ k { f }) from the stack.
 13. Push the values val* to the stack.
 14. Pop the values val^k from the stack.
 15. Return val^k.
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index acdc5cd17b..559d7333e1 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -5,8 +5,6 @@ $ (../src/exe-watsup/main.exe ../spec/wasm-3.0/*.watsup -l --splice-latex -p spe
 == Parsing...
 == Elaboration...
 == IL Validation...
-== Running pass sideconditions...
-== IL Validation after pass sideconditions...
 == Translating to AL...
 == Prose Generation...
 ../spec/wasm-3.0/6-typing.watsup:195.10-195.32: if_expr_to_instrs: Yet `$before(typeuse, x, i)`
@@ -341,6 +339,7 @@ warning: syntax `elemidx` was never spliced
 warning: syntax `eleminst` was never spliced
 warning: syntax `elemmode` was never spliced
 warning: syntax `elemtype` was never spliced
+warning: syntax `evalctx` was never spliced
 warning: syntax `exnaddr` was never spliced
 warning: syntax `exninst` was never spliced
 warning: syntax `export` was never spliced

From c7ddf3b9100e54c0a69c52ce9e57701a36e64e32 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Thu, 29 Aug 2024 20:54:15 +0900
Subject: [PATCH 5/5] Flatten ifs of normal blocks into conjuction

---
 spectec/src/il2al/translate.ml |  3 ++-
 spectec/test-prose/TEST.md     | 19 ++++++++-----------
 2 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index e36e5f080d..0d1a92a6bc 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -1118,9 +1118,10 @@ let rec translate_rgroup' (rule: rule_def) =
   let body_instrs =
     match normal_block_opt, ctxt_block with
     | None, b -> b
+    | Some b, [] -> b
     | Some b1, b2 ->
       (* Assert: b1 must have the else-less IfI as inner most instruction *)
-      insert_instrs_to_else b2 b1
+      insert_instrs_to_else b2 (Transpile.flatten_if b1)
   in
 
   translate_prems pops body_instrs
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 0eae22001b..43c878d39e 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -15636,15 +15636,13 @@ watsup 0.4 generator
 
 #. Pop all values :math:`{{\mathit{val}}^\ast}` from the top of the stack.
 
-#. If :math:`{{\mathit{val}}^\ast}` is not :math:`\epsilon`, then:
+#. If :math:`{{\mathit{val}}^\ast}` is not :math:`\epsilon` and :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
 
-   a. If :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}` is of the case :math:`\mathsf{ref{.}exn}`, then:
+   a. Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
 
-      1) Let :math:`(\mathsf{ref{.}exn}~a)` be :math:`{\mathit{instr}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}`.
+   #. Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
 
-      #) Push the value :math:`(\mathsf{ref{.}exn}~a)` to the stack.
-
-      #) Execute the instruction :math:`\mathsf{throw\_ref}`.
+   #. Execute the instruction :math:`\mathsf{throw\_ref}`.
 
 #. Else if the first non-value entry of the stack is a :math:`\mathsf{label}`, then:
 
@@ -24234,11 +24232,10 @@ Step_read/throw_ref
 4. If instr_u0 is of the case REF.NULL, then:
   a. Trap.
 5. Pop all values val* from the top of the stack.
-6. If (val* is not []), then:
-  a. If instr_u0 is of the case REF.EXN_ADDR, then:
-    1) Let (REF.EXN_ADDR a) be instr_u0.
-    2) Push the value (REF.EXN_ADDR a) to the stack.
-    3) Execute the instruction THROW_REF.
+6. If ((val* is not []) and instr_u0 is of the case REF.EXN_ADDR), then:
+  a. Let (REF.EXN_ADDR a) be instr_u0.
+  b. Push the value (REF.EXN_ADDR a) to the stack.
+  c. Execute the instruction THROW_REF.
 7. Else if the first non-value entry of the stack is a LABEL_, then:
   a. If instr_u0 is of the case REF.EXN_ADDR, then:
     1) Let (REF.EXN_ADDR a) be instr_u0.