formal spec overview for the 3rd exception handling proposal

This is an attempt to formally describe @aheejin's 3rd proposal, which she presented to the Wasm CG, and which was voted to be the new EH proposal, on September 18, 2020. This is not formal spec that I have developed, but a formal description of this 3rd proposal.

This is a reworked form of my [first attempt on this formal spec overview](WebAssembly#87 (comment)) edited with my new understanding of the spec based on the discussion below, and in other issues, and according to @aheejin 's [3rd proposal overview](https://github.com/WebAssembly/exception-handling/blob/f7a4f60d11fb6326fc13f84d3889b11d3873f08a/proposals/Exceptions.md) in PR WebAssembly#137.

This is in the form of a document as @tlively [requested](WebAssembly#142 (comment)), to make discussion on specific points easier.

I wrote this formal spec overview roughly in the style of the 2nd proposal's [formal spec overview](WebAssembly#87 (comment)) by @rossberg.

Particular points of interest:

- In this I assume `rethrow` does have an immediate, as it is now described in WebAssembly#137.
- The instruction `unwind` now reduces to `catch_all ... rethrow` as specified in Heejin's overview.
- Because unwind is much simpler in this MVP, there is no `throw_point` anymore and `caught_m` is much simpler.
- The introduction of `caught_m` now also introduces a label around the catch instructions, which label a rethrow instruction can reference.
- Added explanation of the peculiar side condition in try's execution rule - just trying to make the rules more compact.

I would be happy if anyone could point out things that are wrong or that I misunderstood.

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

@@ -0,0 +1,165 @@
+# 3rd proposal formal spec overview
+
+This is an overview of the 3rd proposal's formal spec additions, to aid in discussions concerning the proposed semantics.
+
+## Abstract Syntax
+
+### Types
+
+Exception Types
+
+```
+exntype ::= [t*] -> []
+```
+
+### Instructions
+
+```
+instr ::= ... | throw x | rethrow l
+        | try bt instr* (catch x instr*)+ end
+        | try bt instr* (catch x instr*)* catch_all instr* end
+        | try bt instr* delegate l
+        | try bt instr* unwind instr* end
+```
+
+### Modules
+
+Exceptions (definitions)
+
+```
+exn ::= export* exception exntype  | export* exception exntype import
+```
+
+Modules
+
+
+```
+mod ::= module ... exn*
+```
+
+## Validation (Typing)
+
+To verify that a `try...delegate l` instruction refers to a label introduced by a try block (I'll call this a try-label), introduce a type attribute to labels in the validation context, which type attribute is set to `try` when the label is a try-label. The original notation `label [t*]` will then be a shortcut for `label {result [t*], type ε}`.
+
+Moreover, to verify that the `rethrow l` instruction refers to a label introduced by a catch block (call this a catch-label), we allow this type attribute of labels in the validation context to be set to `catch` when the label is a catch label. This addition is reflected in the execution rules, by the administrative instruction `caught` which introduces a label around the instructions of the catching try-block's catch instructions.
+
+
+### Instructions
+
+
+```
+C_exn(x) = [t*] -> []
+--------------------------------
+C |- throw x : [t1* t*] -> [t2*]
+
+
+C_label(l).type = catch
+-------------------------------
+C |- rethrow l : [t1*] -> [t2*]
+
+
+bt = [t1*] -> [t2*]
+C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*]
+(C_exn(x_i) = [t'_i*] -> [])^n
+(C, label {result [t2*], type catch} |- instr_i* : [t'_i*] -> [t2*])^n
+(C, label {result [t2*], type catch} |- instr'* : [] -> [t2*])?
+----------------------------------------------------------------------
+try bt instr* (catch x_i instr_i*)^n (catch_all instr'*)? end : bt
+
+
+bt = [t1*] -> [t2*]
+C, label {result [t2*], type try} |- instr* : [t1*] -> [t2*]
+C_label(l).type = try
+------------------------------------------------------------
+try bt instr* delegate l : bt
+
+
+bt = [t1*] -> [t2*]
+C, label {result [t2*], type try} |- instr_1* : [t1*] -> [t2*]
+C, label {result [t2*], type catch} |- instr_2* : [] -> [t2*]
+--------------------------------------------------------------
+try bt instr_1* unwind instr_2* : bt
+```
+
+## Execution (Reduction)
+
+### Runtime structure
+
+Stores
+
+```
+S ::= {..., exn exninst*}
+```
+
+Exception Instances
+
+```
+exninst ::= {type exntype}
+```
+
+Module Instances
+
+```
+m ::= {..., (exn a)*}
+```
+
+Administrative Instructions
+
+```
+instr ::= ... | throw a | catch_n{a instr*}*{instr*} instr* end
+        | delegate{l} instr* end | caught_m{a val^n} instr* end
+```
+
+Throw Contexts
+
+```
+T ::= v* [_] e* | label_n{e*} T end | caught_m{a val^n} T end | frame_n{F} T end
+```
+
+### Instructions
+
+In the following reduction rules, note that `caught_m` introduces a label around the catching instructions. This corresponds to the label a `rethrow l` would target.
+
+
+```
+F; throw x  -->  F; throw a  (iff F_exn(x) = a)
+
+caught_m{a val^n} label_m{} B^l[rethrow l] end end
+  --> caught_m{a val^n} label_m{} B^l[val^n (throw a)] end end
+
+caught_m{a val^n} val^m end  -->  val^m
+```
+
+The requirements below involving `k` are to distinguish between a missing `catch_all` and an existing `catch_all` with no instructions (`nop` is added to the empty instruction set of an existing `catch_all`).
+
+```
+F; val^n (try bt instr* (catch x_i instr_i*)* (catch_all instr'*)^k end)
+  -->  F; catch_m{a_i instr_i*}*{instr''*} (label_m{} val^n instr* end) end
+  (iff bt = [t1^n] -> [t2^m] and (F_exn(x_i) = a_i)* and
+  (if k=1 and instr'*=ε then instr''* = nop)
+  and (if k=1 and inst'*=/=ε then instr''* = instr'*) and (if k=0 then instr''*=ε).
+
+catch_m{a_i instr_i*}*{instr'*} val^m end --> val^m
+
+S; F; catch_m{a_i instr_i*}*{instr'*} T[val^n (throw a)] end
+  -->  S; F; caught_m{a val^n} label_m{} val^n instr_i* end end
+  (iff S_exn(a) = {type [t^n]->[]} and a_i = a)
+
+S; F; catch_m{a_i instr_i*}*{instr*} T[val^n (throw a)] end
+  -->  S; F; caught_m{a val^n} label_m{} instr* end end
+  (iff S_exn(a) = {type [t^n]->[]} and instr =/= ε and for every i, a_i =/= a)
+
+S; F; catch_m{a_i instr_i*}*{ε} T[val^n (throw a)] end
+  -->  S; F; val^n (throw a)
+  (iff for every i, a_i =/= a)
+
+
+val^n (try bt instr* delegate l) --> delegate{l} (label_m{} val^n instr* end) end
+  (iff bt = [t^n] -> [t^m])
+
+catch_m{a_i instr_i*}*{instr*} (label_m{} B^l[ delegate{l} (T[val^n (throw a)]) end ] end) end
+  --> catch_m{a_i instr_i*}*{instr*} label_m{} val^n (throw a) end end
+
+
+try bt instr* unwind instr'* end --> try bt instr* catch_all instr'* rethrow 0 end
+```