From 46d3f9487f8fced0af810b8f393ba2ef0693a2c6 Mon Sep 17 00:00:00 2001
From: "Ioanna M. Dimitriou H" <idimitriou@igalia.com>
Date: Fri, 25 Feb 2022 13:36:29 +0100
Subject: [PATCH 1/3] Fix typing rule of administrative delegate.

This is not the suggestion given in that last review of #143:
https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998

but a potential fix of the issue raised there.
---
 proposals/exception-handling/Exceptions-formal-overview.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md
index 5630083b..baf9bfb9 100644
--- a/proposals/exception-handling/Exceptions-formal-overview.md
+++ b/proposals/exception-handling/Exceptions-formal-overview.md
@@ -83,7 +83,7 @@ C ⊢ try bt instr1* (catch x instr2*)* (catch_all instr3*)? end : [t1*]→[t2*]
 
 C ⊢ bt : [t1*]→[t2*]
 C, labels [t2*] ⊢ instr* : [t1*]→[t2*]
-C.labels[l] = [t*]
+|C.labels| ≥ l
 -------------------------------------------
 C ⊢ try bt instr* delegate l : [t1*]→[t2*]
 ```
@@ -209,7 +209,7 @@ S;C, labels [t2*] ⊢ instr1* : []→[t2*]
 S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*]
 
 S;C, labels [t*] ⊢ instr* : []→[t*]
-C.labels[l] = [t0*]
+|C.labels| ≥ l
 ------------------------------------------------------
 S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]
 

From e11012d9a301484d691884adc996298fa22d149a Mon Sep 17 00:00:00 2001
From: "Ioanna M. Dimitriou H" <idimitriou@igalia.com>
Date: Wed, 17 Aug 2022 17:43:13 +0200
Subject: [PATCH 2/3] Addressed the original review comment, added an
 explanation line.

The original review comment: https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998

The explanation line clarifies what happens if the label targets the frame, and what labels are allowed.
---
 proposals/exception-handling/Exceptions-formal-overview.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md
index baf9bfb9..0b0558ad 100644
--- a/proposals/exception-handling/Exceptions-formal-overview.md
+++ b/proposals/exception-handling/Exceptions-formal-overview.md
@@ -83,11 +83,13 @@ C ⊢ try bt instr1* (catch x instr2*)* (catch_all instr3*)? end : [t1*]→[t2*]
 
 C ⊢ bt : [t1*]→[t2*]
 C, labels [t2*] ⊢ instr* : [t1*]→[t2*]
-|C.labels| ≥ l
+C.labels[l] = [t0*]
 -------------------------------------------
 C ⊢ try bt instr* delegate l : [t1*]→[t2*]
 ```
 
+Note that `try ... delegate 0` may appear without any explicitly surrounding block, in which case the label 0 refers to the label of the frame. Currently it is not allowed to refer to a label higher than the one of the frame.
+
 ## Execution (Reduction)
 
 ### Runtime Structure
@@ -209,7 +211,7 @@ S;C, labels [t2*] ⊢ instr1* : []→[t2*]
 S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*]
 
 S;C, labels [t*] ⊢ instr* : []→[t*]
-|C.labels| ≥ l
+C.labels[l+1] = [t0*]
 ------------------------------------------------------
 S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]
 

From cb5cc85f6d4d1dc0faaa3ddf47cbc29af50e6f4a Mon Sep 17 00:00:00 2001
From: "Ioanna M. Dimitriou H" <idimitriou@igalia.com>
Date: Fri, 26 Aug 2022 10:20:25 +0200
Subject: [PATCH 3/3] Fix typing of administrative delegate.

---
 proposals/exception-handling/Exceptions-formal-overview.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md
index 0b0558ad..027a4720 100644
--- a/proposals/exception-handling/Exceptions-formal-overview.md
+++ b/proposals/exception-handling/Exceptions-formal-overview.md
@@ -210,10 +210,10 @@ S;C, labels [t2*] ⊢ instr1* : []→[t2*]
 -----------------------------------------------------------
 S;C, labels [t2*] ⊢ catch{a? instr2*}* instr1* end : []→[t2*]
 
-S;C, labels [t*] ⊢ instr* : []→[t*]
+S;C ⊢ instr* : []→[t*]
 C.labels[l+1] = [t0*]
 ------------------------------------------------------
-S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]
+S;C ⊢ delegate{l} instr* end : []→[t*]
 
 S ⊢ tag a : tag [t0*]→[]
 (val:t0)*