formal spec overview for the 3rd exception handling proposal

[ioannad]

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 much reworked form of the first attempt on this formal spec overview edited accordingly. It is in the form of a document as @tlively requested, to make discussion on specific points easier.

This formal spec overview is roughly in the style of the 2nd proposal's formal spec overview by @rossberg.

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

[tlively]

Thanks for writing up this updated semantics, @ioannad! This PR will be a useful reference for ongoing discussions.

[aheejin]

Don't formal spec docs live in document/ directory? Do you plan to make a separate "real" formal spec there, and this is something else for discussions?

[tlively]

I like having this document available for discussion because it is much easier to read and much more focused on EH issues than the raw formal spec documents would be.

[ioannad]

@aheejin

Don't formal spec docs live in document/ directory? Do you plan to make a separate "real" formal spec there, and this is something else for discussions?

I put this together with the "English spec overview" because I thought of this as also an overview (a formal version), because it's written in Markdown, because it contains all the exception handling (EH) additions (except opcodes) and only the EH additions, and because its purpose is just for the discussions, until we reach consensus on its contents. When there is consensus on these contents, then I will update the "real" formal spec, which is more involved, with formatting and prose.

I could move it somewhere in the document/ directory if you prefer that, but I'm not sure where.

Or I could instead update document/core/appendix/index-instructions.rst, document/core/appendix/index-rules.rst, and document/core/appendix/index-types.rst, which contain an overview of the types and validation rules, but there is no such collection for the execution rules. I could even make a new document in the appendix, containing a, *.rst "cheatsheet" (or an "exception handling cheatsheet") which contains everything, but even then, for these file/s to be readable we'd have to build the documentation, and any comments on the PR changes would be less clear.

WDYT?

[aheejin]

Oh, sorry, now I understand, and I think having an introduction for the formal spec here is good.

[aheejin]

So the intention here is, as in the case of delegate, rethrow can target any label including labels for blocks, loops, and try-delegates, but they are just validation failures, right?

The concept of catch label is a little new. Can we consider it in the same as try label? Then we have this problem:

try $label0
  rethrow $label0  ;; cannot be done, because it's not within catch below
catch
end

But delegate has another problem anyway if it we say it takes a try block:

try $label0
catch
  try
    ...
  delegate $label0  ;; cannot be done, because $label0's catch is not below but above here
end

delegate can be considered to target a catch label too, but in this case it can be considered to target try:

try $label1
  try $label0
    try
      ...
    delegate $label0
  delegate $label1
end

So my question is

1. For rethrow: If we introduce a concept of catch label, should we also mention that that this works in the same way as its corresponding try block for other branch-like constructs?
2. For delegate: The concept of try block may not work in something like my second example, but as we can see in my third example, it is different from catch label. Should we introduce a new concept?

I might be mistaken on something, so please let me know.

[aheejin]

Gentle ping :)

[ioannad]

Sorry I'm late replying @aheejin!

The concept of catch label is a little new. Can we consider it in the same as try label? Then we have this problem:

try $label0
  rethrow $label0  ;; cannot be done, because it's not within catch below
catch
end

I used catch labels just as a helper to make sure that the rethrow is inside a catch block, not as something one can use in the text format. In your example, rethrow is not inside a catch block, so that example would not validate.

So, to your question 1, I did not intend a catch label to be the same as a try label.

I'm not sure I understand the problem with delegate, I'll try to look at this again later today or tomorrow.

[ioannad]

@aheejin I see now what you mean, yes, you are right.

In the second example, the label from the catch block would interfere with delegate, when it shouldn't. Also rethrow should not interfere with other labels, it should just count the stack of nested catch blocks it is in - to rethrow an exception, an exception must be caught, so we can only rethrow n the exception caught by the nth surrounding catch block.

I think to solve this, the catch-labels should be removed, and a separate concept of a caught-stack should be added to the runtime, described by a parallel to blocks:

C^0 ::= val^m [_] instr
C^{n+1} ::= caught{exnaddr val^k} C^n end

Also a new stack caught to validation contexts, which gets an element "caught" prepended whenever we catch an exception by a catch block.

About the 3rd example, did you omit a catch in the outer try block on purpose, meaning that trys without catches could be allowed, as @tlively suggested in #131 ? In that case, in your 3rd example, if we replace ... by throw $exn then the example would reduce to throw $exn. I think it would be a nice simplification to the syntax to allow catchless try blocks. They are equivalent to try ... catch_all rethrow 0 end AFAICT, so no new behaviour would be introduced with this simplification.

If we additionally allow delegate to target any label, as @RossTate suggested, then we can have the same effect also without a try block, as he noted, and we wouldn't have to make any changes to labels. I admit I am not so fond of adding this auxiliary information to labels, I just thought I had to.

To clarify I'll commit the changes I'm suggesting later today, in three separate patches:

1. add caught-stack to the runtime and to validation contexts and remove catch-labels (which actually should have been called "caught" labels but anyway)
2. allow trys without catches
3. remove auxiliary type of labels and allow delegate to reference any label

WDYT?

[ioannad]

I just pushed the promised commits. The first one's commit message contains the question "Should the administrative instruction caught be removed from the right hand side of rethrow's execution step?", because I ran out of time and I won't be able to think about it until the end of next week. Does anyone have any thoughts on this?

[ioannad]

@aheejin: I just want to clarify that the commits I pushed are just so that it's clear what I meant with my comment above. These commits are independent from each other, so one could be accepted and the next one not without trouble, I think.

[aheejin]

Sorry for the delayed reply. The catch-less try was a typo, sorry. I didn't mean we have a catchless try. We can maybe consider it, but I personally have a preference against it, as I said in #131. What I tried to convey in that third example was that we can't make delegate target outer catch, because delegte can also target an outer try-delegate.

[RossTate]

There is no need for delegate to specifically reference a try block. That is, delegate does not mean to use a particular handler but rather to ignore the handlers in between. (I suspect delegate will likely be implemented either by subtracting code ranges or by popping handlers depending on the backend.) Such a relaxation is also helpful, as one can skip over all handlers, i.e. delegate to the caller, without having to wrap the function body with a try and an empty handler.

[RossTate]

Suggested change

	C, label [t2*], caught all |- instr_2* : [] -> [t2*]
	----------------------------------------------------
	try bt instr_1* unwind instr_2* : bt
	C, label [t2*] |- instr_2* : [] -> []
	----------------------------------------------------
	try bt instr_1* unwind instr_2* end : bt

This was discussed in #142, but just to reiterate for the sake of having this suggestion be self contained: A purpose of unwind is to specify unwinders in a way that works well with non-exceptional non-local control constructs. To that end rethrow should not work within unwind (which was the case in the earlier formalization), as it may not make sense to rethrow other non-local control constructs from within a different dynamic scope. Instead, unwind automatically resumes unwinding at the end, and so instr_2* does not need to output [t2*].

[ioannad]

Issue #142 is still open, and (unfortunately) it does not seem to me that there is general agreement on unwind. About the return values, in the closed issue #129, it seems it was decided that unwind blocks should indeed return values.

About rethrow in unwind blocks or not, I can't find that discussion, can you please link to it?

By the way, the earlier formalisation was wrong, as it did not reflect the spec that @aheejin presented and that we voted on.

[ioannad]

Thank you for catching the missing end typo!

[ioannad]

@RossTate, about the unwind block's instructions returning values or not: now I see that I was perhaps too quick to close #129, since you don't seem to agree with @aheejin's proposal there. Since unwind ends with a rethrow 0, any return values seem indeed unnecessary to me as well. @aheejin what do you think? The try block can still have any blocktype, it's just that the unwind block's instr_2 shouldn't return any values, since they will be discarded by the rethrow in the end anyway.

Having said that, either way it doesn't seem to make much of a difference. Even if instr_2* returns any values, even not matching t2*, even then it wouldn't really make a difference, I think.

[ioannad]

@RossTate about rethrow inside an unwind block's instr_2*, I can't see much difference from having a throw inside instr_2*. Looking around the issues, I only saw arguments saying that a rethrow would end the unwinding process, but so would a br or throw or return. I didn't manage to find a discussion wrt rethrow of other non-local control constructs. Please help me out find the relevant comments/discussions, I'm a bit lost in the several issues containing mixed information.

Having said that, please note that the rethrow 0 resulting from the current unwind, is creating a new exception, so it's throwing within a different dynamic scope, IIUC. I do understand that unwind should probably be laid out more carefully than what we do here, and this is exactly why I suggested that we postpone it to an extension of the MVP, to avoid making mistakes we can't take back anymore, wrt backwards compatibility. I don't think that people should expect the MVP to be WebAssembly's "final word on exceptions" (or non-local control flow in general - as @phoe suggested), but the "first word on exceptions" (or non-local control flow). :)

But, as @aheejin says, I'm also ok to keep unwind, if it helps us get the spec settled soon so we can continue our implementations. (Btw, @takikawa and I already started landing first patches for try-catch and throw in SpiderMonkey.)

[aheejin]

If we can place br that returns a value within unwind, I'm not sure why the type of unwind block has to be [] -> []?

[rossberg]

br and the block's end are control paths with different targets in the case of unwind, so they have different type constraints (that's also the case with loop btw). An unwind block will drop any remaining value on the floor at end, so it's pointless to require any values there -- all that would do is force producers to push dummy values for no reason.

[tlively]

Sorry I'm late to the party here, but I would expect all three of @takikawa's examples to validate because of implicit unreachable polymorphic behavior due to the implicit rethrow at the end of the unwind clause, just as they would if the rethrow were made explicit as a separate instruction at the end of the block.

[rossberg]

@tlively, that would be possible as well, but is useless in this case, since unlike branches or throws, an end cannot occur in the middle of a larger "expression". Stack polymorphism is useful for examples like

(... larger exp (i32.div_u (x) (br_if $bailout (i32.eqz (y))) (y)) ...)

or something like that. That cannot be constructed with a delimiter like end.

Not saying that we can't do it, but it would be a (minor) relaxation without practical value.

[tlively]

I agree there’s no practical value. Not making that relaxation would be fine with me.

[aheejin]

Sorry for the delayed reply. The catch-less try was a typo, sorry. I didn't mean we have a catchless try. We can maybe consider it, but I personally have a preference against it, as I said in #131. What I tried to convey in that third example was that we can't make delegate target outer catch, because delegte can also target an outer try-delegate.

[aheejin]

This seems we are using a regular labels for delegate. Can we handle this case then?

try $label0
catch
  try
    ...
  delegate $label0  ;; cannot be done, because $label0's catch is not below but above here
end

Is this in line with the @RossTate's suggestion? His suggestion looks like we don't need to use labels at all. Am I interpreting it correctly, @RossTate?

[RossTate]

That's in line with my suggestion. The number just indicates how many syntactic enclosures to skip out of. A convention in the text format could be that you can label a syntactic enclosure and reference that label in the delegate rather than have to compute the number of syntactic enclosures between.

[aheejin]

@ioannad What do you think? If we are on the same page on this I'll update the explainer to match this.

[ioannad]

@aheejin, @RossTate, that sounds good to me!

@aheejin, the example you gave above is now correctly illegal (not translatable to integer labels, as you suggested), because the catch-labels are now removed.

[aheejin]

Sorry what I meant was not catch label but try label. In my example the label $label0 is attached to try. So it should be a valid try label, but the code itself should be invalid. I'm not sure how you can describe that code using try label, and that's the question I asked.

Did your last commit contain any changes related to this? I don't see any, so...

[ioannad]

@aheejin, apologies for the late response. Let me start by saying that I do agree that your example should be impossible. Thank you for clarifying, I see what the problem is, and I also see that we actually do need caught to have a label after all, in order to accommodate situations such as:

try bt
  throw $e
catch $e
  ....
  br 0 ;; ---
end   ;;    |
;; <------- break to here

Tricky situation, I'll have to think about how to express this formally.

[aheejin]

@ioannad Not sure if I understand. Why is br 0 a problem here? br can use try labels just like block labels because try can also serve as a block. Did you try to write delegate 0 instead in your last example?

Maybe we can just do away with labels for delegate definition as @RossTate suggested.

[aheejin]

Just to check if we are in the same page, here are questions. I'll write my current state of understanding. Please let me know if it doesn't match with yours.

try
  block
    try
      throw $e
    delegate N
  end
catch
end

In this code, N == 0 targets the block so it is a validation failure. N == 1 targets the outer catch so it is fine. N == 2 means the exception should be rethrown to the caller. All other values are validation failure. I think this behavior is in line with the explanation here:

That is, delegate is essentially saying "for any exceptions thrown from in here, pretend their continuation does not include the n+1 immediately enclosing control constructs".

try
catch                    ;; outer
  block
    try
    catch               ;; inner
      rethrow N
    end
  end
end

In my understanding, in this code, N == 0 rethrows the exception caught by the inner catch and N == 1 rethrows the exception caught by the outer catch. All other values of N are validation failure. @ioannad's formal spec here also assumes rethrow only targets caught label (which is an imaginary label for the spec writing purpose), I think this is in line with what @ioannad wrote.

Is my understanding for both problems correct?

CC'ing other people who are working on the VM implementation to be sure. @thibaudmichaud @takikawa

---

Edit: The rethrow rule I described in this example turns out to be incorrect. Please refer to #146 (comment) for the discussions.

[thibaudmichaud]

In this code, N == 0 targets the block so it is a validation failure

I interpreted @RossTate's comment:

there is no need for the target to be a try. That is, catch_br is essentially saying "for any exceptions thrown from in here, pretend their continuation does not include the n+1 immediately enclosing control constructs".

to mean that targeting a non-try block is valid and delegates to the next enclosing try-catch block. In your example this would mean that N=0 is the same as N=1. The implementation would be trivial to fix so I am not advocating for one interpretation over the other, I just want to make sure we are on the same page too.

I thought N=2 would be a validation failure since it does not target a try-catch block. Delegating to the caller also makes sense but I would like to know if there is a motivation for it, since it requires some special case in the implementation.

[RossTate]

I believe one of the use cases is to delegate to the caller, so I had in mind that N==2 would be fine. Otherwise I echo what @thibaudmichaud said about N==0.

[aheejin]

I also think either interpretation of N == 0 is fine. @ioannad, do you have any preference?

@thibaudmichaud The functionality to rethrow to the caller is necessary. This instruction was basically added to solve unwinding mismatch problems after control flow linearization by placing block, try, and end markers, and mismatches can occur at any level; a throwing instruction that targets catch can end up being caught by another catch, while another instruction that does not target any catch in the current function (which ends up throw to the caller) can also end up being caught by another catch, so it is just the same problem manifest in two different way. I should've made this clear in the explainer, sorry. Can we make N == 2 throw to the caller in the V8 implementation?

[ioannad]

I agree with all your (latest) interpretations of @aheejin's examples. So I agree that these examples should be as @aheejin expects, except that in the first example N==0 and N==2 are not validation errors and N==2 rethrows to the caller.

I tried to write down these and other example reductions to add to the formal-overview document, but I have still to figure out some subtleties with the labels and delegate, as I mentioned in this comment above. However, I am on holidays until the end of the year, so I'll come back with an updated formalism in early 2021. :)

[aheejin]

I agree with all your (latest) interpretations of @aheejin's examples. So I agree that these examples should be as @aheejin expects, except that in the first example N==0 and N==2 are not validation errors and N==2 rethrows to the caller.

Yes, in my first example I also wrote N==2 rethrows to the caller and not a validation failure.
I wrote N==0 was a validation failure, but I'm also OK with @thibaudmichaud's interpretation that we can treat N==0 to have the same semantics as N==1.

However, I am on holidays until the end of the year, so I'll come back with an updated formalism in early 2021. :)

Happy holidays!

[thibaudmichaud]

Happy new year!
Thanks for the clarifications, I will update the V8 implementation to support the N==2 case.

[backes]

Happy new year everyone!

Thanks for the clarifications in this thread! I like the N == 2 case, but I have a slight preference to make N == 0 a validation failure (i.e. disallow targetting anything but a try block). This would allow us to skip a scan through the control stack in the VM (to find an outer try block), and would remove an unnecessary ambiguity in program representations.

[takikawa]

Happy new year folks. I was on holiday so I missed the ping on this thread, but I agree with @backes about the N == 0 case being easier to implement as a validation failure. Otherwise everything sounds good to me as well.

[ioannad]

Hi all,

apologies for the long delay, among other things I got caught up with starting to implement the proposal in IonMonkey (WIP).

I just pushed a version of the formal spec that I think matches @aheejin's #137 and the current consensus.

I also added a new file with examples from comments in issues and what these examples reduce to, to make sure everyone is happy with the spec. The first example I made up to include all new instructions, and it's the only one with a full reduction trace.
With this I am hoping that it's easy to quickly see how this all works technically, even for those who haven't spent much time with the formal spec.

I'd be happy to get any corrections, suggestions, reviews etc.

[rossberg]

This looks great! Just a few minor oversights, I think. And some minor simplifications you could make.

[rossberg]

Same here, the first premise about C_label(l) is redundant.

[rossberg]

Don't you need to extend B^k with caught for this to be correct?

I'm not sure why it's B^{l+1} instead of B^l, though.

[ioannad]

To be honest this has been bothering me lately: as it is now, even in the main spec, any instructions could be between two labels in a B^l, or am I misunderstanding something?

Unless you mean that rethrow's immediate l should only count the catches, which is not the case anymore (I missed this at first as it's a bit hidden in a different issue).

[ioannad]

I used B^{l+1} because B^0 does not contain / is not pointing to- a label, while rethrow 0 should point to a surrounding label.

Also note that, in the execution rules, caught_m gets introduced with a label after it (the +1), to compensate for the evaporating try-label when catching the exception by a handler. Does this make sense?

[rossberg]

To be honest this has been bothering me lately: as it is now, even in the main spec, any instructions could be between two labels in a B^l, or am I misunderstanding something?

Not sure I follow. A branch can skip over any instruction. What would be an example of an odd context?

I used B^{l+1} because B^0 does not contain / is not pointing to- a label, while rethrow 0 should point to a surrounding label.

Intuitively, the B^l captures the l label binders that you skip over with a branch. So if l=0 then this context should indeed not contain any label. The target label is the one explicit in the rule, surrounding B.

However:

Also note that, in the execution rules, caught_m gets introduced with a label after it (the +1), to compensate for the evaporating try-label when catching the exception by a handler. Does this make sense?

Ah, yes, this explains why we need a +1 here: the catch actually is outside its associated label, so we actually need to skip over that as well to get to the catch.

It's a bit odd, though. I suspect that this use of labels creates an issue with the soundness proof. In particular, what is the administrative typing rule for catch_n? It can't bind the label, since that is bound by label_n. But label_n won't attach the catch kind, so any contained rethrow won't type-check anymore after reducing try to catch, and we lose preservation.

Maybe this can be hacked by changing the reduction rule for try-catch so that it binds the label outside the catch. Then the typing rule for catch_n could amend the label kind of the innermost label in its environment. (And we wouldn't have the +1.)

Something to think about. I'd encourage you to write out the typing rules for the administrative instructions, to check that it all hangs together.

(I guess the more baroque nature of the new design is showing here.)

[rossberg]

:)

[rossberg]

To be honest this has been bothering me lately: as it is now, even in the main spec, any instructions could be between two labels in a B^l, or am I misunderstanding something?

Not sure I follow. A branch can skip over any instruction. What would be an example of an odd context?

I used B^{l+1} because B^0 does not contain / is not pointing to- a label, while rethrow 0 should point to a surrounding label.

Intuitively, the B^l captures the l label binders that you skip over with a branch. So if l=0 then this context should indeed not contain any label. The target label is the one explicit in the rule, surrounding B.

However:

Also note that, in the execution rules, caught_m gets introduced with a label after it (the +1), to compensate for the evaporating try-label when catching the exception by a handler. Does this make sense?

Ah, yes, this explains why we need a +1 here: the catch actually is outside its associated label, so we actually need to skip over that as well to get to the catch.

It's a bit odd, though. I suspect that this use of labels creates an issue with the soundness proof. In particular, what is the administrative typing rule for catch_n? It can't bind the label, since that is bound by label_n. But label_n won't attach the catch kind, so any contained rethrow won't type-check anymore after reducing try to catch, and we lose preservation.

Maybe this can be hacked by changing the reduction rule for try-catch so that it binds the label outside the catch. Then the typing rule for catch_n could amend the label kind of the innermost label in its environment. (And we wouldn't have the +1.)

Something to think about. I'd encourage you to write out the typing rules for the administrative instructions, to check that it all hangs together.

(I guess the more baroque nature of the new design is showing here.)

[ioannad]

Thank you so much @rossberg for the review and ongoing discussion. I pushed the changes you suggested, and I will take a closer look at the typing of the administrative rules and the implications for the soundness proof.

[aheejin]

Sorry it was Thanksgiving holidays and I was OOO for some more days! I'll take a final look shortly.

[aheejin]

Sorry for the long wait! Most of the comments are just simple uppercase/lowercase spelling nits, but I still have some questions. Please bear with me if they are too basic, as I haven't spent much time with formal semantics 😅

[aheejin]

By the way does this support val* between label_n and catch_m/caught_m/delegate? For example,

val* (label_n{instr*} (catch_m{ tagaddr? instr* }* B^k end) end

This is supported, but

val* (label_n{instr*} val* (catch_m{ tagaddr? instr* }* B^k end) end

is this supported? Or should we?

[ioannad]

This is supported, but

 val* (label_n{instr*} val* (catch_m{ tagaddr? instr* }* B^k end) end

is this supported? Or should we?

The formal-overview does support this, but I can't see any way to reduce to it.
AFAICT I don't think it is a problem to support this case, even if it were possible.

[aheejin]

My question was, I didn't think the current block context rules can produce

val* (label_n{instr*} val* (catch_m{ tagaddr? instr* }* B^k end) end

meaning val* between a label and catch/caught/delegate. I might have been mistaken. But I think what was suggested in #143 (comment) can create this sequence, so I don't think this will be a problem.

[rossberg]

Sorry for being late as well!

[rossberg]

I believe this should actually be

Suggested change

	C.labels[l] = [t'*]
	C.labels[l+1] = [t'*]

Otherwise, it would be referring to a different label than the original try-delegate.

[ioannad]

@rossberg: I think the +1 is missing because of the behaviour of "breaking inside the label". This way we also cover the case of delegating to the function body. WDYT?

[rossberg]

Are you sure? If you have

try ... delegate $l

you'll reduce to

label{} (delegate{$l} ... end) end

When you type this, the outer label adds an entry to the labels environment before you get to this typing rule, unlike with the try-delegate before the reduction. So you have to skip over that prior label in this rule.

[ioannad]

@rossberg Apologies for the delay, last week ended up unexpectedly way too full.

Is it possible that the +1 you're missing is hidden in the labels [t*] attached to C in the other two judgements? The typing rule for try-delegate gives exactly the premises of this typing rule for adm.delegate, which in turn matches the typing for adm.label, to derive the type for that last expression in the end - I think.

More concretely, if I'm not mistaken, in your question we have a derivation of

(1)   C ⊢ try bt instr* delegate $l : []→[t^n]

and because try bt instr* delegate $l reduces to label_n{} (delegate{$l} instr* end) end we should be able to derive that C ⊢ label_n{} (delegate{$l} instr* end) end : []→[t^n].

If this is what you ask to show, then from the derivation of (1) we know the following.

(2)   C ⊢ bt : []→[t^n]
(3)   C, labels [t^n] ⊢ instr* : []→[t^n]
(4)   C.labels[l] = [t'*]

By having (3) and (4) as the premises for the typing rule of adm.delegate we derive

C, labels [t^n] ⊢ delegate{l} instr* end : []→[t^n]

which we can use as a premise to the typing rule for adm.label to get the desired

C ⊢ label_n{} (delegate{l} instr* end) end : []→[t^n]

WDYT?

[rossberg]

The problem I see is that (4) is not the premise you'll need when arriving at the adm.delegate rule. Instead you'll need

(4') C'[l'] = [t'*]

with C' = C, labels [t^n] and some l', because that's the context you now enter the rule with. The only suitable l' that allows you to prove this from (4) is l+1, I believe.

[aheejin]

If we change the current rule

F; val^n (try bt instr* delegate l)
  ↪ F; label_m{} (delegate{l} val^n instr* end) end

to

F; val^n (try bt instr* delegate l)
  ↪ F; delegate(l) (label_m{} val^n instr* end) end

meaning, if we put the label created by the try-delegate itself within the scope of adm.delegate, can this confusion be helped?

[ioannad]

Continuing the discussion with a suggestion in #205 .

[ioannad]

Apologies again for the many "single comments" (which I realised send lots of notification emails, oops). I will bundle my responses with the "submit review" feature.

There are still a couple of comments I haven't replied to yet, but will do by tomorrow the latest.

[aheejin]

@ioannad Are you planning to land this soon? I think we can address a few things mentioned in the latest round and land this.

[ioannad]

Apologies for the long delay @aheejin! I am now available again for this. My plan is to finish by Monday adjusting the last bits we talked about, then we can finally land this.

I will then update the formal document #180, possibly initially without the prose (just rebase and update to reflect the recent changes of this formal-overview). Filling in the prose and last couple of details in the formal document should not take more than 1-2 weeks I think, and I would probably prefer to do that in a separate PR, (we could talk about this in #180 if necessary)

[ioannad]

Pushing these changes shortly.

Apologies for the delay, I am feeling unwell this week. Will still need a couple weeks for the formal document but counting from now.

[ioannad]

@aheejin @rossberg : I merged the current stand of this repo and went through all the discussions once more to make sure I didn't forget anything, resolving what was obviously resolved.

If you are ok with my answers to the couple of unresolved conversations, I think we can go ahead and merge this. Updating #180 to reflect this formal overview will follow shortly after that (partially without prose first, PR with the rest hopefully by next week).

[ioannad]

@rossberg: I think the +1 is missing because of the behaviour of "breaking inside the label". This way we also cover the case of delegating to the function body. WDYT?

[ioannad]

Can we consider this resolved, or am I missing the error?

[ioannad]

This PR has so many comments it's become difficult to navigate. Since we agree at least 99% that this is ok I'll go ahead and merge it. If something needs to be changed still, it could be part of a followup. Thank you for the reviews and discussions!

[rossberg]

Sorry for being late, I have a couple of follow-up comments.

[rossberg]

Suggested change

	C, labels catch [t2*] ⊢ instr'* : [t*]→[t2*])*
	(C, labels catch [t2*] ⊢ instr''* : []→[t2*])?
	C, labels (catch [t2*]) ⊢ instr'* : [t*]→[t2*])*
	(C, labels (catch [t2*]) ⊢ instr''* : []→[t2*])?

[rossberg]

You also modify the definition of C on line 46. Maybe move that here as well?

[rossberg]

Are you sure? If you have

try ... delegate $l

you'll reduce to

label{} (delegate{$l} ... end) end

When you type this, the outer label adds an entry to the labels environment before you get to this typing rule, unlike with the try-delegate before the reduction. So you have to skip over that prior label in this rule.

[ioannad]

Sorry I didn't wait longer @rossberg ! Tomorrow I'll make a new PR with your suggestions and take a closer look to the typing rule for the administrative delegate. If in the meantime you see something else that should go in that next PR, please feel free to comment here with it.

Btw soon I will be pushing an update to #180 to adjust for the changes on the merged part of this PR, but I will update that tomorrow as well with your latest suggestions. (Seems to be taking a bit longer, will update that in the coming day or two.)

[aheejin]

Sorry for the late reply! Thanks for merging; it looks good to me. I made a few cosmetic fixes in #204.