Addressed latest review and added the missing +1 to the adm. delegate.

The latter matches the interpreter implementation in PR WebAssembly#175

Author: ioannad

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

@@ -39,7 +39,7 @@ Take the frame `F = (locals i32.const 0, module m)`. We have:
 
 ```
 ↪ ↪ ↪ F; label_1{} (catch_1{a_x local.get 0}
-           (label_0{} (delegate{0}
+           (label_0{} (delegate{1}
              (label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0}
                throw a_x end) end) end) end) end) end
 ```
@@ -48,12 +48,12 @@ For the empty throw context `T = [_]` the above is the same as
 
 ```
 F; label_1{} (catch_1{a_x local.get 0}
-     label_0{} (delegate{0}
+     label_0{} (delegate{1}
        label_0{} (catch_0{i32.const 27 local.set 0 rethrow 0}
          T[throw a_x] end) end) end) end) end
 
 ↪ F; label_1{} (catch_1{a_x local.get 0}
-       (label_0{} (delegate{0}
+       (label_0{} (delegate{1}
          (label_0{} (caught{a_x} i32.const 27 local.set 0 rethrow 0
            end) end) end) end) end) end
 ```
@@ -62,33 +62,25 @@ Let `F'` be the frame `{locals i32.const 27, module m}`, and let `B^0 = [_]`.
 
 ```
 ↪ F; label_1{} (catch_1{a_x local.get 0}
-       (label_0{} (delegate{0}
+       (label_0{} (delegate{1}
          (label_0{} (caught{a_x} B^0 [rethrow 0]
            end) end) end) end) end) end
 
 ↪ F; label_1{} (catch_1{a_x local.get 0}
-       (label_0{} (delegate{0}
+       (label_0{} (delegate{1}
          (label_0{} (caught{a_x} B^0 [throw a_x]
            end) end) end) end) end) end
 ```
 
-Let `T' = label_0{} (caught{a_x} B^0 [_] end) end`.
+Let `T' = label_0{} (caught{a_x} [_] end) end`, and `B^1 = label_0 [_] end`.
 
 ```
 ↪ F; label_1{} (catch_1{a_x local.get 0}
-       (label_0{} (delegate{0}
-         T'[throw a_x] end) end) end) end
+       (B^1 [delegate{1}
+         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; 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
+       (throw a_x) end) end
 
 ↪ F; label_1{} (caught_1{a_x} local.get 0 end) end
 

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

@@ -165,7 +165,7 @@ S; F; catch_m T[val^n (throw a)] end
 
 
 val^n (try bt instr* delegate l)
-  ↪ label_m{} (delegate{l} val^n instr* end) end
+  ↪ label_m{} (delegate{l+1} val^n instr* end) end
   (if bt = [t^n]→[t^m])
 
 delegate{l} val^n end ↪ val^n
@@ -190,7 +190,7 @@ S;C, labels [t*] ⊢ catch_n{a? instr'*}* instr* end : []→[t*]
 S;C, labels {result [t*], kind try} ⊢ instr* : []→[t*]
 C.labels[l].kind = try
 -----------------------------------------------------------------------
-S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]
+S;C, labels [t*] ⊢ delegate{l+1} instr* end : []→[t*]
 
 S.tags[a].type = [t'*]→[]
 (val:t')*
@@ -199,11 +199,3 @@ S;C, labels {result [t*], kind catch} ⊢ instr* : []→[t*]
 S;C, labels [t*] ⊢ caught_m{a val^n} instr* end : []→[t'*]
 ```
 
-By adding the attribute `kind` to labels, we are creating situations in the proof of type preservation, where we have a derivation of some `S;C, label [t*] ⊢ instr* : []→[t*]` but we need to have that `S;C, label {result [t*], kind <labelkind>} ⊢ instr* : []→[t*]` for some `<labelkind> ::= try | catch`. To resolve this we add the following typing rule for labels in the context, which ensures our newly introduced `try` and `catch` blocks can contain any instructions a regular block can.
-
-```
-S;C, label [t*] ⊢ instr* : []→[t*]
-labelkind = try ∨ labelkind = catch
------------------------------------------------------------
-S;C, label {result [t*], kind labelkind} ⊢ instr* : []→[t*]
-```