`anyref` == `externref` introduces a typesystem mode

[titzer]

I didn't notice this until I updated Wizard after #271, which makes externref an alias for anyref. Unfortunately a consequence of this is that, from a Wasm binary's perspective, funcref (-0x10), which was previously not a subtype of externref (-0x11), is now a subtype of (-0x11), though we've got a different text-level name for it. We've changed the meaning of that binary type.

That introduces a mode in the engine; if the engine supports the GC proposal, then (-0x10) <: (-0x11), and if not, then (-0x10) </: (-0x11).

The only clean way I saw to resolve this, if an engine wants to support the current spec, but also a proposal in the works, is to model all the types, i.e. both externref and anyref, as before, but the mode flag flips the meaning of (-0x11).

The same thing will happen, but worse, with function-references. We currently don't have subtyping between function types, but we'll want to add it in the future. That'll be another mode flag that changes the type system underneath.

We need to be careful how we introduce type relations.

[titzer]

It might also be that another alternative would be to lift this change to the function-references proposal.

[conrad-watt]

The only clean way I saw to resolve this, if an engine wants to support the current spec, but also a proposal in the works, is to model all the types, i.e. both externref and anyref, as before, but the mode flag flips the meaning of (-0x11).

I think this touches on something we've perhaps implicitly formed opinions about, but not explicitly discussed in detail: do we consider adding additional subtyping relations between existing types to be a backwards-compatible change (in the sense of WebCompat)?

Previous conversations on funcref <: anyref suggest that we have been thinking of this as allowable, because it was suggested that we could conservatively not have this subtyping relation and then add it later if it proved necessary. If we believe this, then it's not very important that an engine support both the "current" and "future" (extra subtyping relation) spec at once via flags - the engine should be able to just switch entirely to the "future" spec without causing any issues for existing code (edit: modulo issues of standardisation/shipping which are common to all proposals).

In combination with the floated idea of having ref.cast for any heaptype, I could imagine a WebCompat hazard to do with adding some new B <: A relation. One could imagine an "anyref downcast and dispatch" function which takes an anyref and does something like

br_on_cast A ...
<otherwise>
br_on_cast B ...

and then adding B <: A could cause weird behavioral changes if, as a result, a B that used to be handled by the second case becomes handled by the first case. I think the change to unify externref and anyref is safer than this general case though, because (IIUC) no code exists that will attempt to downcast to externref. (edit: I've not thought about how the proposed changes in function-references would interact with the above example).

[rossberg]

@titzer, sure, whenever we extend the type system, and you want to maintain the prior semantics for a while, you'll need a temporary version flag. But that isn't specific to subtyping, is it? Basically, any new rule of syntax or semantics may potentially have to go behind such a flag. Consider the example of generalising the type of an instruction.

In this particular case, isn't it sufficient to simply make the allowance of funcref <: externref dependent on that flag? Or is that what you mean with "flip the meaning of -0x11"?

[rossberg]

@conrad-watt, I believe it's fairly uncontroversial that only those changes qualify as backwards-compatible that either

1. Make a previously malformed/invalid program valid.
2. Make a previously trapping program non-trapping.

These conditions ensure that a language change does not change the behaviour of a previously existing, successfully executing program.

(FWIW, the latter condition is justified by our description of traps as program bugs and the inability to catch traps in Wasm. It would become less viable if we did support such recovery. Though the line is blurry, of course, since you can recover in the host.)

I believe that adding new subtype relations between types that didn't exist before should be fine in that regard. That would allow us to refine the type hierarchy in the future with new types (e.g., the addition of a func_or_data heap type or other intermediate types).

The observation here is that adding funcref <: anyref may be different, because it adds a subtype relation between existing types, and that may change the behaviour of an existing program because we can successfully test for this relation at runtime.

However, I don't think that's actually the case. Because as long as you didn't have funcref <: anyref, the static type system as currently defined would prevent you from even attempting a downcast between them! So you could not yet express that program that would change its meaning later, and once you can, it can't change anymore.

Of course, that is not true in general, so we will have to be careful about what subtype relations we are adding. But I do believe that all additions that make a previously unrelated type a subtype of anyref should be fine. More generally, I'd expect that it's unproblematic to zip previously disjoint type hierarchies as long as that does not affect the subtyping within each of the hierarchies.

[titzer]

But I do believe that all additions that make a previously unrelated type a subtype of anyref should be fine.

I don't think this is the case. As @conrad-watt points out, a program that does a case-based analysis on anyref (with ref.is and ref.as) could suddenly go from being exhaustive (i.e. covering all possible subtypes of anyref), to not covering all cases, even without introducing any new types.

Put simply, a program that was happy (and correct) to process a single anyref, or an array of them, or a table of them, with branches over all legal subtypes at the time, could now encounter values that it couldn't possibly have before. Moreover, if we disallow illegal casts, such a program cannot even future-proof itself in anticipation of subtyping rules changing.

[rossberg]

[Dang, I'm again not getting github notification emails.]

Interesting point, but given that anyref is inhabited by host types, you can never assume that any case analysis expressible in Wasm is exhaustive. Unless you control all the possible values flowing into it, but then there is no problem with the described scenario, because the new cases can't come up.

[titzer]

The more I think about this, the more I think it is potentially serious module interoperability problem. In particular, I think I agree that a single module (without JIT) won't have its behavior change due to a future spec change adding new subtyping relationship between existing types, because that module would not have validated before.

However, a philosophical point is that a static type annotation T means both "a T is legal here" but also "nothing I know about that is unrelated to T is legal here".

The scenario arises between modules or interacting with hosts. Here, a module's static types are meant to describe the legal values that it accepts. So for example, if X </: T and a module exports a function f that accepts a T, it is pointedly declaring that it is not legal to pass an X, or any other type </: T. If the type system changes so that X <: T, then a new module, validated under the new rules, or the host, could pass X. This will break f. Philosophically, we might blame the caller of f, but in reality f could pass these Ts deep down inside, through many calls or indirections, squirreling them away for later in a table or field, etc, or even pass them on to yet another module. Then the point at which something finally goes wrong may happen way, way, in the future, where code had assumed X couldn't happen trips over one. Then it isn't even attributable to the function f or its caller anymore.

I think that violates the spirit of static type annotations.

If we disallow (currently) illegal casts and tests, then the f in the scenario above can't even defend itself dynamically.

[rossberg]

It comes down to the difference between open and closed unions/variants. You are right in the cases where T is a closed union, i.e., a module consuming it is in its right to assume that there is a known, closed set of cases.

However, anyref is not a closed type. It deliberately is an open union, since the host is already allowed to introduce additional cases. For a module to make the assumption that it has covered "all cases" of an outside anyref is wrong by definition. For an open union, one must always assume the existence of cases one doesn't know about. Whether these cases are host-infused or Wasm-from-the-future does not make a difference.

I believe this can be made formally precise with the right (infinite) model of anyref.

[titzer]

The issue isn't the appearance of new, unknown cases, e.g. a new Y <: T appearing. It's that by design the module's previous static type annotations disallowed X where T occurs, but a future type system change allows X where T occurs.

[rossberg]

Old code cannot tell that the unknown case it encounters is an X, no more than it can recognise a new Y. It will necessarily treat both the same way, entirely opaquely. Consequently, I don't see how the difference matters?

[tlively]

Here's my understanding of the issue (assuming references to all heap types are inhabitable and that all cast instructions have nontrapping variants):

Given the current rules back compat rules, adding X <: Y where previously X </: Y is unsafe iff there was previously a cast instruction testing heaptype(x: ref X) <:? Y.

If we have a cast instruction that checks heaptype(x: ref X) <:? Y for arbitrary reference type x and heap type Y, then this implies that we can never introduce X <: Y where previously X </: Y and that's the end of the story.

Otherwise, it is possible in principle for a program to prove by case analysis that heaptype(x: ref X) </: Y even when there is no cast testing heaptype(x: ref X) <:? Y directly, so introducing X <: Y would violate the program's intent, even though it would not change the program's behavior.

Defining Y to be an "open" variant addresses this by saying, "well actually, that program never proved heaptype(x: ref X) </: Y in the first place, so it was buggy all along."

Another nearly-equivalent solution would be to explicitly add "We are allowed to introduce X <: Y where previously there was no cast instruction testing heaptype(x: ref X) <:? Y" to our list of back-compat rules, which would make the program correct for a particular version of Wasm but explicitly not forward-compatible.

Another alternative would be accept the program's intent as valid and promise, "we will never introduce X <: Y where a program could have previously proved directly or indirectly that X </: Y.

None of these solutions is obviously correct, but we would want to pick one and document it clearly.

---

Personally, I would prefer to sidestep the whole issue by providing a cast instruction that checks heaptype(x: ref X) <:? Y for arbitrary X and Y. Not being able to introduce new subtype relations on existing types seems fine to me. If we ever find that we want to introduce such a subtype relation, we can create a new type for which the subtype relation holds with conversion instructions to and from the old type for which the subtype relation does not hold. That's messy, but I don't expect it to come up.

[rossberg]

None of these solutions is obviously correct

I beg to differ. Until you consider side effects, especially control effects, you can easily make backwards compatibility fairly precise:

• No execution path valid in version N of a language must, under version N+1 of the language, (a) change its behaviour for inputs already possible in version N (except where it previously trapped), or (b) encounter new behaviours or new results for inputs not yet possible in version N (such as traps).

In the case where Y is an open type (which is the case for anyref, because we explicitly specify it to include arbitrary external types) this makes introducing new subtype relations a compatible change as long as there previously was no way to test that subtype relation.

(Note that "version" involves both Wasm and corresponding host APIs, e.g., when calling back to the host, although what's considered "valid" in the host language may be a bit more fuzzy. Further, note that I'm not saying anything about execution paths involving code not valid in version N, e.g., when a version N module calls out to unknown version N+1 code. In that case, all bets are off. We have already excepted that as a fact of life for other extensions, e.g., exceptions. It is generally impossible to guard against unknown features in future callee code, unless we introduced a complex, fine-grained effect system to Wasm, which I am convinced would be impractical.)

Personally, I would prefer to sidestep the whole issue by providing a cast instruction that checks heaptype(x: ref X) <:? Y for arbitrary X and Y.

That would not side-step the issue at all, it just would make it more severe. ;)

FWIW, for types that are part of the same hierarchy, you can always test their relation already. It may require more than one instruction, but that's irrelevant to the question at hand.

For types that are not part of the same hierarchy, providing a cast does not make sense, since that would require a compatible representation between the two. Since the whole point of splitting hierarchies like anyref and funcref would be to enable different representations, a cast would defeat the purpose of such a split. Unless it is defined to always fail, now and for all eternity, but then, what's the point of providing such a completely useless instruction?

[conrad-watt]

Given the current rules back compat rules, adding X <: Y where previously X </: Y is unsafe iff there was previously a cast instruction testing heaptype(x: ref X) <:? Y.

To echo @rossberg (IIUC?), I think it only makes sense to allow a cast A B "cast (static types) A to B" instruction if it's statically validated that A is a supertype of B, so the situation wouldn't be quite as bad as we seem to be thinking. With this restriction, it's hard to express a program that semantically relies on a subtyping relation not being present, which is why my example above was so convoluted, and I don't think the scenario I sketched applies to the future introduction of func <: any.

With reference to @titzer's comment, this scenario seems to me to be OK from a WebCompat perspective no matter what downcasts we have since, as noted, code at rest will never make use of the new subtyping relation (because it wouldn't previously have validated). It feels more like an ABI compatibility issue where two modules produced under two different sets of features (and presumably compiler versions) interact in an unfortunate way. Even then, the older module can defend itself with a default/unknown case, which seems natural to insert anyway if you're attempting to exhaustively downcast.

[rossberg]

It feels more like an ABI compatibility issue where two modules produced under two different sets of features (and presumably compiler versions) interact in an unfortunate way. Even then, the older module can defend itself with a default/unknown case, which seems natural to insert anyway if you're attempting to exhaustively downcast.

Exactly. If the older module does not have that default case, then it can already fail in the exact same way in the old language version, e.g., when passed an external anyref. That is, the ABI incompatibility is either an implementation bug on part of one module or an intentional incompleteness protected by an informal contract, but that contract can already be violated.