[interpreter] Reject subtypes with multiple supertypes

[sanguineman]

Summary

WebAssembly allows a subtype to refer to a previously declared parent type as its supertype. The current specification restricts a subtype to have at most one direct supertype.

It also notes that future versions of WebAssembly may allow subtypes to have more than one supertype.

The validation specification written in SpecTec correctly enforces this restriction by requiring the number of direct supertypes to be at most one.

rule Subtype_ok:
  C |- SUB FINAL? (_IDX x)* comptype : OK(x_0)
  -- if |x*| <= 1 ;; restricts the number of supertypes to be at most one
  -- (if x < x_0)*
  -- (if $unrolldt(C.TYPES[x]) = SUB yy* comptype')*
  ----
  -- Comptype_ok: C |- comptype : OK
  -- (Comptype_sub: C |- comptype <: comptype')*

However, the OCaml reference interpreter does not check the number of direct supertypes. It only iterates over the supertype list and validates each referenced type individually.

let check_subtype (c : context) (sut : subtype) at =
  let SubT (_fin, uts, ct) = sut in
  List.iter (fun ut -> check_typeuse c ut at) uts; (* does not check the number of supertypes here *)
  check_comptype c ct at

Consequently, the reference interpreter accepts subtype definitions with multiple direct supertypes, even though the current declarative specification requires them to be rejected.

This PR adds the missing cardinality check to check_subtype. It also adds a regression test containing two valid non-final parent struct types and a child type that directly inherits from both. The module is rejected specifically because the child has more than one direct supertype.

Testing

• make -C interpreter test/gc/type-subtyping
• make -C interpreter unittest