[spec] Disagreement between the textual description and the formule rule for br_on_non_null's validation

[4y8]

The validation rule for br_on_non_null states in the textual format that the last type of the result type corresponding to the given label should be ref null? ht. However, in the formal rule, it can't be null and is forced to be ref ht.

None of the test I saw used it with a label of type ref null? ht (it would be useless actually).

The reference validator seems to accept ref null ht, as the test done is a matching and ref ht <= ref null ht.

I can do a PR where the formal rule is modified if that can help.

[rossberg]

Actually, I think the formal rule is unintentionally restrictive here and should also use null?. At the same time, the interpreter should implement the rule more faithfully, without peeking at the stack.

[4y8]

I agree on both points. I am writing a wasm validator (which is why I submit all these PRs with typos) and I currently implement this rule by making sure the type t_l (the last one in the result of the label) is a reference type (without any condition on its nullability), and then making sure the type on top of the stack matches ref null ht where ht is the heaptype underlying t_l.

[rossberg]

PTAL at #1940.