[P1] ensures are enforced on all returns, including recoverable error returns

[ngmachado]

Problem

Postconditions are injected before every return without distinguishing success returns from error returns.

Impact

Contracts that intend “success-postconditions” fail on legitimate error-return paths.

Describe the runtime, correctness, security, or DX impact.

Acceptance Criteria

Define semantics explicitly:

• success-only ensures, or result-conditional ensures (is_ok(result) => ..., is_err(result) => ...).
• Lowering honors the chosen semantics.
• Add regressions covering both success and error exits.