Inline expansion loses early-return semantics when branch conditions are non-exhaustive

[adust09]

Summary

https://github.com/leanEthereum/leanMultisig/blob/43205ce23924c05183174fc1b698f55e0265f64f/TODO.md?plain=1#L87

What I’ve tried

• Active flag approach: Introduced a guard variable that gets set to 0 after a return, expecting later statements to be skipped. This failed because the VM forbids overwriting the same memory slot (SSA), so the guard cannot be toggled from 1 to 0.
• Jump/Label approach: Replaced each inlined return with jump end_label. Although this preserves control flow in theory, we still assign directly into the caller’s result variable on every return path; the SSA invariant breaks when different paths try to write different values,
  and runtime fails with Computation invalid.