Validation reference algorithm `push_ctrl` mistakenly pushes parameters too

[Swiftb0y]

The validation algorithm from the appendix contains a (afaict superflous) push_vals(in):

https://github.com/WebAssembly/spec/blob/abc8d16dcb4b36f818af9ee2fa9b1bf0b50503cb/document/core/appendix/algorithm.rst?plain=1#L112-L115

This does not match the prose description following:

https://github.com/WebAssembly/spec/blob/abc8d16dcb4b36f818af9ee2fa9b1bf0b50503cb/document/core/appendix/algorithm.rst?plain=1#L132-L133

Based on my personal understanding this would mean that during execution the functions parameters are already on the stack. This also conflicts with the reduction of invoke: https://github.com/WebAssembly/spec/blob/abc8d16dcb4b36f818af9ee2fa9b1bf0b50503cb/document/core/exec/instructions.rst?plain=1#L2973-L3011

Am I correct in the assessment that the push_vals(in) in the reference algorithm is simply incorrect and should be removed? Thank you.