Requiring descriptors to have matching finality

[tlively]

We could optionally require a descriptor type to be final if and only if its described type is final. With the fixed validation rules from #58, it's impossible to define a subtype of either an open described or descriptor type if the other is final, so in practice one being final makes the other final. Requiring them both to be explicitly final in that case makes it slightly simpler for the engine to optimize casts, etc.

cc @Liedtke, @jakobkummerow

[tlively]

I'm inclined to resolve this without making any changes; i.e. by continuing to allow mismatched finality. Obviously toolchains should emit both types as final if possible (and Binaryen's --type-finalizing pass will do this when it can assume a closed world), but if the toolchain does the optimal thing, there's no additional benefit to having the toolchain check that the finalities match.

[Liedtke]

My feeling is that some basic consistency shouldn't be an optimization but just a requirement for a module to be valid. It would be nice if the absence of final would mean non-final / extensible. Toolchains and engines already need to check consistency between descriptors and described structs (due to the subtyping requirements), so checking the finality as well (which is a part of subtyping) would just make sense?

[tlively]

We're both on the same page that it's essentially down to a matter of taste, right? If you assume that toolchains can be responsible for doing the optimal thing, then the only implementation difference is whether or not engines have to do this extra check during validation. I believe we've tended to resolve this kind of choice by not requiring the engine to do extra checks, but the extra check probably makes no difference in practice.

[Liedtke]

We're both on the same page that it's essentially down to a matter of taste, right?

Yes.

If you assume that toolchains can be responsible for doing the optimal thing, then the only implementation difference [...]

Agreed, for the implementation a "we don't care about any inconsistencies" is even nicer. From a language perspective I think it's much worse because it makes it more difficult to reason about the semantics of specific types imo. But then, this is just my opinion and I am not an expert in type systems or language design. It just seems the cleaner solution to disallow inconsistent states. (I'd call having a non-final type that is "de facto" final inconsistent.)

[Liedtke]

As a happy coincidence, just 1 hour after writing this comment, I reviewed a fuzzer change.
The fuzzer wants to generate a subtype of a Wasm struct. Right now without descriptors it does that by searching for Wasm struct types which fulfill:

!desc.hasUnresolvedSelfReferences() && !desc.isFinal

(desc is the struct description. The name description is confusing now but it's older than the existence of the Custom Descriptors proposal. hasUnresolvedSelfReferences is an internal fuzzer limitation we haven't addressed, yet.)

Now this becomes:

!desc.hasUnresolvedSelfReferences() && !desc.isFinal
    && (desc.describes == nil || !desc.describes!.isFinal)
    && (desc.descriptor == nil || !desc.descriptor!.isFinal)

So for the fuzzer the current relaxation is a net-negative. As the fuzzer generates descriptor + described pairs in one generation step, having to restrict it to consistent finality OTOH would not add any complexity.
I wouldn't be surprised if toolchains also had to check these conditions, so binaryen might also need to handle this? Or does Binaryen just "fix" these inconsistencies in the beginning? I guess, it can't because that would change the types and depending on the use case the type section needs to be stable for linking with other modules?

CC @leonbett

[tlively]

I wouldn't be surprised if toolchains also had to check these conditions, so binaryen might also need to handle this?

Binaryen's fuzzer avoids that particular complexity. Because it wants to generate arbitrary recursive types with interesting subtyping, it needs to generate a "plan" for the kinds (e.g. struct, array, func) and relationships (e.g. subtypes, descriptors) between types before figuring out the details of each type definition. When we get to generating the definitions, we know whether a type will have no subtypes, in which case we can independently flip a coin to say whether it's final or not. Requiring matching finality or not would make no change to complexity.

Similarly, I would expect no change in complexity for module producers, since they will already be marking both types final, or alternatively letting Binaryen handle finality.

So I would be surprised if matching finality made any difference in complexity for producers or toolchains (besides your fuzzilli example, of course).

---

I've added this to the list of custom descriptors issues to discuss and try to resolve at the CG meeting tomorrow. Maybe other folks have opinions about the color of this bikeshed :) If there's a general feeling that it would be nicer to require the finalities to match, I'm happy to go with that.

[tlively]

We discussed this briefly at the CG meeting today and nobody else had an opinion (let alone a strong opinion) either way. @Liedtke and I discussed this some more offline and decided to keep the status quo of allowing mismatched finality.

[rossberg]

Hm, we otherwise require the subtype hierarchies to be in lock-step. It seems dubious not to extend this requirement to finality. I can't point my finger at a concrete problem, but hygiene suggests the conservative choice and not allow it.

[tlively]

I don't know, we have the square rule governing supertype declarations, but that's it. We don't require the fields of descriptor and described types to match in any way, and I don't see why finality would be any different. OTOH we do expect to require sharedness to match once we also have shared objects.

[tlively]

#112 implements this change if we do decide we want it, but I remain skeptical.

[rossberg]

What I mean is, it follows from the other rules that both subtype chains have to have the exact same shape, i.e.,

A  < B  < C  < top
|    |    |     |
A' < B' < C' < top

where X' is the descriptor type for X. Or can one extend further to the right? If not, it seems odd to not also demand, essentially, symmetric "bot <" on the left end of both rows.

[tlively]

It is already impossible to have one of the described and descriptor hierarchies extend below the other. That is a consequence of the square rule and does not require the declared finalities to match.