Implemented latest review comments and updated.

In particular:
- The labels surrounding try-catch and try-delegate now get a standard
  label in the first step, which is then refined to catch-labels and/or
  try-labels per subblock.
  + For that I allowed the new administrative instructions to appear
    nested directly inside a label_n{} in block contexts.
  + Also added a validation rule to the administrative label_n{}.
  + Due to this, all block contexts appear now without a successor
    exponent.
- Updated to latest try-catch syntax described in issue WebAssembly#157.
- Corrected some previously wrong syntax.
- Removed try-unwind (...) as per issue WebAssembly#156
- Updated Exceptions-formal-examples.md similarly.

Author: ioannad

proposals/exception-handling/Exceptions-formal-examples.md

@@ -12,21 +12,22 @@ If anyone would like that I add another reduction trace, or other examples, plea
 
 ### notation
 
-If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F_exn(x) = a_x`, where `F` is the current frame.
+If `x` is an exception index, then `a_x` denotes its exception tag, i.e., `F.exception[x] = a_x`, where `F` is the current frame.
 
 ## example 0
 
-The only example with an almost full reduction trace, and all new instructions (`rethrow` and `catch_all` are hidden in `unwind`'s reduct). The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown.
+The only example with an almost full reduction trace, and all new instructions. The first 3 steps, reducing the several `try`s to their respective administrative instructions, are not shown.
 
 ```
 (func (result i32) (local i32)
   try
     try
       try
         throw x
-      unwind
+      catch_all
         i32.const 27
         local.set 0
+      rethrow 0
       end
     delegate 0
   catch x
@@ -37,48 +38,59 @@ The only example with an almost full reduction trace, and all new instructions (
 Take the frame `F = (locals i32.const 0, module m)`. We have:
 
 ```
-↪ ↪ ↪ F; catch_1{a_x local.get 0} (label_1{}
-           (delegate{0} (label_0{}
-             (catch_0{i32.const 27 local.set 0 rethrow 0} (label_0{}     ;; the try-unwind
+↪ ↪ ↪ F; label_1{} (catch_1{a_x local.get 0}
+           (label_0{} (delegate{0}
+             (label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0}
                throw a_x end) end) end) end) end) end
-
 ```
 
-For the throw context `T = label_0{}[_]end` the above is the same as
+For the empty throw context `T = [_]` the above is the same as
 
 ```
-F; catch_1{a_x local.get 0} (label_1{}
-     (delegate{0} (label_0{}
-       (catch_0{i32.const 27 local.set 0 rethrow 0}
+F; label_1{} (catch_1{a_x local.get 0}
+     label_0{} (delegate{0}
+       label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0}
          T[throw a_x] end) end) end) end) end
 
-↪ F; catch_1{a_x local.get 0} (label_1{}
-       (delegate{0} (label_0{}
-         (caught{a_x} (label_0{} i32.const 27 local.set 0 rethrow 0
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         (label_0{} (caught{a_x} i32.const 27 local.set 0 rethrow 0
            end) end) end) end) end) end
 ```
 
-Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^1 = label_0{} [_] end`.
+Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]`.
 
 ```
-↪ F'; catch_1{a_x local.get 0} (label_1{}
-       (delegate{0} (label_0{}
-         (caught{a_x} B^1 [rethrow 0] end) end) end) end) end
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         (label_0{} (caught{a_x} B^0 [rethrow 0]
+           end) end) end) end) end) end
 
-↪ F'; catch_1{a_x local.get 0} (label_1{}
-       (delegate{0} (label_0{}
-         (caught{a_x} B^1 [throw a_x] end) end) end) end) end
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         (label_0{} (caught{a_x} B^0 [throw a_x]
+           end) end) end) end) end) end
 ```
 
-Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`.
+Let `T' = label_0{} (caught{a_x} B^0 [_] end) end`.
 
 ```
-↪ F'; catch_1{a_x local.get 0} (label_1{}
-       (delegate{0} T'[throw a_x] end) end) end
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         T'[throw a_x] end) end) end) end
 
-↪ F'; catch_1{a_x local.get 0} (label_1{} throw a_x end) end
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         T'[throw a_x] end) end) end) end
 
-↪ F'; caught_1{a_x} (label_1{} local.get 0 end) end
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       (label_0{} (delegate{0}
+         T'[throw a_x] end) end) end) end
+
+↪ F; label_1{} (catch_1{a_x local.get 0}
+       T'[throw a_x] end) end
+
+↪ F; label_1{} (caught_1{a_x} local.get 0 end) end
 
 ↪ ↪ ↪ i32.const 27
 ```
@@ -87,32 +99,38 @@ Let `T' = label_0{} (caught{a_x} B^1 [_] end) end`.
 
 ### example 1
 
-Interaction of `rethrow` with `unwind`. Taken from [this comment](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-705586912) by @rossberg.
+Location of a rethrown exception.
 
 ```
 try
+  val1
   throw x
 catch x
   try
-    instr1*
-    rethrow 0
-  unwind
-    instr2*
+    val2
+    throw y
+  catch_all
+    try
+      val3
+      throw z
+    catch z
+      rethrow 2
+    end
   end
 end
 ```
 
-Assuming `instr1*` and `instr2*` don't throw another exception, this example reduces to
+In the above example, all thrown exceptions get caught and the first one gets rethrown from the catching block of the last one. So the above reduces to
 
 ```
-caught_0{a_x} (label_0 {}
-  (caught_0{a_x} (label_0 {}
-    instr2* throw a_x end) end) end) end
+label_0{} caught{a_x val1}
+  val1 (label_0{} caught{a_y val2}
+    (label_0{} caught{a_z val3}
+      val3 val1 (throw a_x) end end)
+        end end) end end)
 ```
 
-which in turn reduces to `throw a_x`.
-
-Note that any global state changes due to `instr1*` or `instr2*` will take place.
+which in this case is the same as `val1 (throw a_x)`.
 
 ### example 2
 
@@ -137,7 +155,7 @@ This is a validation error (no catch block at given rethrow depth).
 
 ### example 3
 
-`delegate` targetting a catch is a validation error.
+`delegate` targeting a catch is a validation error.
 
 ```
 try $label0
@@ -152,93 +170,23 @@ This is a validation error because `delegate`'s `$label0` refers to the catch-la
 
 ### example 4
 
-`delegate` correctly targetting a `try-delegate` and a `try-catch`.
+`delegate` correctly targeting a `try-delegate` and a `try-catch`.
 
 ```
 try $label1
   try $label0
     try
       throw x
-    delegate $label0
-  delegate $label1
+    delegate $label0 ;; delegate 0
+  delegate $label1 ;; delegate 1
 catch x
   instr*
 end
 ```
 
-The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to
+The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to the following.
 
 ```
-caught_0{a_x} (label_0 {} instr* end) end
-```
-
-
-## interaction of `delegate` and `unwind`
-
-Two examples from issue #130.
-
-### example 5
-
-The [opening example](https://github.com/WebAssembly/exception-handling/issues/130#issue-713113953)
-of issue #130.
-
-```
-i32.const 11
-global.set 0
-try $l
-  try
-    try
-      throw x
-    delegate 1
-  unwind
-    i32.const 27
-    global.set 0
-  end
-catch_all
-end
-global.get 0
+label_0 {} (caught_0{a_x}  (label_0 {} instr* end) end
 ```
 
-Here, `delegate 1` targets the label `$l` (so it would be the same if we wrote `delegate $l` instead).
-
-This example returns `11`, because `delegate` skips everything up to and not including `try $l`.
-
-### example 6
-
-This example
-[appears to keep](https://github.com/WebAssembly/exception-handling/issues/130#issuecomment-704249682)
-the issue #130 open.
-
-@RossTate expressed concerns with respect to an example possibly equivalent to
-the one below. "Possibly", because the original example in the comment refers to
-an `unwinding` branch, first presented in issue #124, so I attempted to rewrite
-the example to match the current syntax as best I could.
-
-```
-try $t
-  try $l
-    try $u
-      try
-        throw x
-      delegate $t
-    unwind
-      instr1*
-    end
-  catch x
-    instr2*
-  end
-  instr3*
-catch_all
-  instr4*
-end
-```
-
-The thrown exception tag `a_x` is delegated to the outer `try $l - catch_all`, ignoring the `try $u - unwind` and `try - catch x` in between. So this example reduces to
-
-```
-caught_0{a_x} (label_0{} instr4* end) end
-```
-
-During the above reduction, `instr1*`, `instr2*`, and `instr3*` are never executed.
-
-