The definition of validation of br_table is inadequate about spec HOT 3 CLOSED

The problem is that it is unclear what is intended by "corresponding" in the spec.

That is the type in the j-th position, i.e., 𝑡_𝑗 and 𝑡'_𝑖𝑗 are in the same position in their respective vectors. That wording is used in other places of the spec as well. I suppose it is unclear here due to the missing precondition that 𝑡* and C.labels[𝑙_𝑖] have the same length. Please see #1709 for a fix.

from spec.

Just to unpack this a little more, instead of "all labels have the same type" it would be more precise to say "all labels are supertypes of the current stack type" - the reason that the linked test validates is because in unreachable code, there's a conceptual "bottom" type which is a subtype of both f32 and f64, so effectively the current stack is typed as [⊥], and we have [⊥] <: [f32] and [⊥] <: [f64].

In particular the following wouldn't validate:

(module
  (func (export "meet?")
    (block (result f64)
      (block (result f32)
        (f32.const 0) (f64.const 0)
        (br_table 0 1 1 (i32.const 1))
      )
      (drop)
      (f64.const 0)
    )
    (drop)
  )
)

from spec.

Thank you!

from spec.