tracking: Lean and Why3 (experimental) backends drop return control flow — early returns silently mis-emitted #624

What

The Lean and Why3 source-emitter backends (both experimental per docs/CAPABILITY-MATRIX.adoc) lower a return expression to just its operand:

• lib/lean_codegen.ml:62 — | ExprReturn (Some e) -> gen_expr e
• lib/why3_codegen.ml:68 — | ExprReturn (Some e) -> gen_expr e

This discards the non-local control transfer. For a tail-position return e in a pure expression target that is harmless, but for a statement-position / early return (e.g. a guard that returns before the rest of the block) the emitted Lean/Why3 keeps executing the remainder of the block — a silent wrong-output miscompile.

Class

A broader codegen-honesty gap than #555 (which fenced effect handlers). Flagged, not yet fenced. Low priority — these are experimental backends, not the reference WASM target — but it violates the project's "fail loud, never silent" rule.

Suggested fix

Mirror the #555 remedy: emit a loud UnsupportedFeature for early/statement-position return in these backends until real control flow is modelled (e.g. lower to an exception/option in Why3, or a do-block early-exit in Lean). Cheapest correct step is the loud fence.

Status

Listed under "Still open" in docs/SOUNDNESS.adoc.

Filed from the docs-soundness pass (PR #622).