Module verify 

Bytecode stack-depth verifier — the third --strict check from #347 A2.

Walks every function’s instruction stream, tracking the abstract stack depth through each opcode and branch. Reports a StackError when two paths into the same program counter carry different depths, which would mean a prior match arm leaked (or over-consumed) values and left the stack in an inconsistent state for subsequent arms.

The check is lightweight: it is a single linear pass with a small worklist. No allocation beyond Vec is needed.

Known sound over-approximation

Return and Panic terminate the function; their successors are not added to the worklist. TailCall is treated like Return. This means dead code after a Return / Panic is not checked — intentional.

Structs

StackError

Functions

verify_function

Verify a single function. Appends to errors.

verify_program

Verify all functions in a slice. Returns one error per inconsistent merge point found.