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 elib/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).
What
The Lean and Why3 source-emitter backends (both experimental per
docs/CAPABILITY-MATRIX.adoc) lower areturnexpression to just its operand:lib/lean_codegen.ml:62—| ExprReturn (Some e) -> gen_expr elib/why3_codegen.ml:68—| ExprReturn (Some e) -> gen_expr eThis discards the non-local control transfer. For a tail-position
return ein a pure expression target that is harmless, but for a statement-position / earlyreturn(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
UnsupportedFeaturefor early/statement-positionreturnin these backends until real control flow is modelled (e.g. lower to an exception/option in Why3, or ado-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).