Lost stack values when entering a loop

(module
  ;; Iterative factorial without locals.
  (func $pick0 (param i64) (result i64 i64)
    (local.get 0) (local.get 0)
  )
  (func $pick1 (param i64 i64) (result i64 i64 i64)
    (local.get 0) (local.get 1) (local.get 0)
  )
  (func (export "fac-ssa") (param i64) (result i64)
    (i64.const 1) (local.get 0)
    (loop $l (param i64 i64) (result i64)
      (call $pick1) (call $pick1) (i64.mul)
      (call $pick1) (i64.const 1) (i64.sub)
      (call $pick0) (i64.const 0) (i64.gt_u)
      (br_if $l)
      (drop) (return)
    )
  )
)

(assert_return (invoke "fac-ssa" (i64.const 25)) (i64.const 7034535277573963776))

After fac-ssa gets invoked and the loop instruction is reached, the two values that have been pushed onto the stack disappear when we enter the loop, so then the subsequent call to $pick1 doesn't have any parameters to use.

The spec

Our rule:

https://github.com/runtimeverification/wasm-semantics/blob/ad238ca2f73ea866b54b31308326ac2a56e64159/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md?plain=1#L549-L552

It looks like the spec states that the stack values are prepended to the instructions when entering the block, but we aren't doing that here.

Start with the embedded fac-ssa WebAssembly module and assertion, then inspect pykwasm/kdist/wasm-semantics/wasm.md at lines 549-552 alongside the linked loop-entry rule in the specification. Reproduce the invocation and verify that the loop preserves the two stack values needed by $pick1 and that the factorial assertion passes.