WebAssembly 3.0 type questions

[zherczeg]

(module
  (table 0 i32 (ref.null func))
)

This is reported as a SyntaxError. Is this mean that in both in text and binary format the non-reference types must be rejected before validation (malformed input)? The 3.0 spec says "The reference type is valid.", but it might refer to actual references only.

(module
  (func $f (param (ref struct)) (result (ref array))
    local.get 0
    ref.cast (ref array)
  )
)

Why this is valid?

[rossberg]

It looks like you just got the syntax wrong. You probably meant

(module
  (table i32 0 (ref null func))
)

which validates fine.

[zherczeg]

I am working on a parser. The old code throws an error during validation (=invalid), but it seems the spec interpreter throws syntax error (=malformed). There are other spec tests which test malformed/invalid modules, but I could not find a particular test for this.

[rossberg]

What "old code" are you referring to? The example in the OP never was syntactically legal, so I'm not sure how it could even reach validation. The reference type, when spelled correctly, is valid in there.

[zherczeg]

Then it is a bug in the old code. I just wanted to confirm it. Thank you for the help.

What do you think about in the second question?

[rossberg]

Hm, can you elaborate why you believe that it should not be valid? Because struct is not a supertype of array?

The implicit source doesn't need to be a supertype of the target type of a cast, they only need to have a common supertype (i.e., be in the same subtype hierarchy). As a general rule, we must always allow a value of subtype to be legal where a supertype is expected. That e.g. is to enable certain code transformations (like inlining) that might lift more tightly typed code into casts where they result in such a case. Technically, that's also needed for soundness, since type preservation of reduction would fail otherwise.

Consider e.g. this example:

(func $f (param $x anyref) ... (if ... (ref.cast arrayref (local.get $x))) ...)
(func $g (param $y structref) ...)
(func $h (param $z structref) (call $g (local.get $z)) (call $f (local.get $z)))

The call to $f in $h is perfectly legal. And it should be fine to inline $f without making it impossible to type the resulting code.

[zherczeg]

Your example is a little different form mine, since null value can be part of structref and arrayref, and that is why casting is possible, even if it is not too practical.

If I understand correctly, the specification specifies the C |- rt <= rt' condition where rt' comes from the stack, and rt is the cast target. The anyref(stack) -> arrayref(expected) matches to this, and perfectly makes sense. As for structref and arrayref, the only common value is none, although it is not clear to me that none is a real value like null. In this case however, why there is a <= validation check, since none is a common value for everything.

[rossberg]

I just used anyref and friends for brevity, it is no different for non-null types.

In the typing rule for ref.cast, rt' can be any supertype of "what is on the stack", since subsumption can always be applied (per the third of the rules for instruction sequences).

Concretely, in your example, (local.get 0) has principal type ε → (ref struct), but by subsumption, can also be given a supertype like ε → (ref any). And with that, the sequence (local.get 0) (ref.cast (ref array)) is perfectly well-typed according to the rule for casts.

Note how the linear validation algorithm handles that (or rather, the analogous case for ref.test) by simply checking the operand type against the top type of the hierarchy.

The type none indeed is uninhabited, i.e., there are no values with that type. So in my inlining example above, assuming $f isn't buggy, the if leading to the cast presumably cannot be reached for the call site in $h and becomes dead code after inlining and specialising the parameter type. If reached, the cast would unconditionally fail, but that's fine as far as Wasm is concerned.

[rossberg]

FWIW, @tlively recently requested a similar relaxation for br_on_cast, see WebAssembly/custom-descriptors#37, implemented in WebAssembly/custom-descriptors#38, since it simplifies Binaryen.

[zherczeg]

Thank you, I think I understand it now.

There is an image in the GC proposal:

      any  extern  func
       |
       eq
    /  |   \
i31  struct  array

Basically there are 3 major types: any, extern, func and any two references in these groups can be the source and target of a cast.

So this is also valid, although the cast will fail:

  (type $t1(func (param i32)))
  (type $t2(func (param i64)))
  (func $f2 (param (ref $t1)) (result (ref $t2))
    local.get 0
    ref.cast (ref $t2)
  )

Btw what is the difference between eq and any?

[zapashcanon]

Btw what is the difference between eq and any?

eq are references that can be tested for physical equality (using ref.eq)

[rossberg]

FWIW, there is a fourth hierarchy in Wasm 3.0, namely exn, which was introduced with exception handling. There might be more in the future, e.g. cont in the stack switching proposal.

[zherczeg]

I have another question:
https://github.com/WebAssembly/spec/blob/wasm-3.0/test/core/gc/ref_cast.wast#L49

The ref.extern 0 is passed as argument, then it is converted by any.convert_extern to any, then it is stored in a table. My problem is, that in our system extern 0 is a function, so it cannot be converted to any. It seems the spec expects this operation to be successful. What should happen exactly here?

This is coming from the execution of the instruction:
(ref.extern addrref) any.convert_extern -> addrref

What should happen if addrref is not a struct/array/i31?

[rossberg]

The notation (ref.extern 0) is wast syntax to create some host value, identifiable by the number. A host running wast can implement these values in whatever way it wants, they must merely be distinguishable from externalised Wasm values and from each other by their numeric argument.

I'm afraid I don't understand what you mean when you say "extern 0 is a function". But note that all values that the host allows under type extern must be convertible to any and back.

[zherczeg]

I thought extern is an external compatible representation of a wasm reference. If an extern can always be converted to any, does it limits its value to array/struct/i31? Or do you need a non-webassembly "type" code which is not accessible from wasm (i.e. it can be converted to any, but all casts must fail, since its representation is unknown. Does this value need to be eq compatible or not?

I can understand the concept of a value outside the scope of wasm (extern value), but converting it to any type is a strange operation for me.

[rossberg]

I thought extern is an external compatible representation of a wasm reference.

The opposite. It is a host pointer/value represented inside Wasm, in its most efficient representation (which may or may not point to a Wasm object). The type already existed in Wasm 2.0, before Wasm even had its own reference values.

Or do you need a non-webassembly "type" code which is not accessible from wasm (i.e. it can be converted to any, but all casts must fail, since its representation is unknown.

Yes. In an implementation where Wasm and host pointers have different representations or live in different heaps, this essentially boxes the external pointer into an internal Wasm heap object.

I can understand the concept of a value outside the scope of wasm (extern value), but converting it to any type is a strange operation for me.

This is so that one can define module import interfaces whose functions operate on some abstract reference (of type any), in such a way that they can be implemented as either a Wasm or a host module. Important for polyfilling or self-hosting scenarios.