[spec] Function validation regression?

[zilinc]

I'm not entirely sure about it, but maybe #2162 has introduced some regression.

A sample module is:

(module (start $f) (func $f (drop (ref.func $f))))

which is supposed to fail validation, due to undeclared function reference. I think in Module_ok, when checking the bodies of the functions in the module, it's under a wrong context with more refs.

In my animated meta-interpreter,

(module (func $f (drop (ref.func $f))))

fails as expected, but the above is not rejected. Of course it could be an error in my manual animation of the circular Module_ok rule, but still I don't see in the declarative rule how it can be rejected.

@rossberg Any thoughts?

[rossberg]

This whole ref declaration hack is a neverending source of joy. We have gone back and forth on what constitutes an implicit ref decl, but if both the test suite and reference interpreter agree that start should not count, then the spec should better match that reality. Can you do a PR to revert that part of #2162?