v0.0.176

Call-site precondition checking now covers calls in statement position (#730).

A call whose result is discarded — a bare consume(need_pos(@Nat.0)); statement — was never checked against the callee's requires(...): the verifier's body translation skipped statement-position expressions, so vera verify reported clean while the precondition went unchecked (a Tier-0 silent failure). Statement-position expressions are now verified, restoring the "contracts checked at every call site" guarantee.

Two narrower boundaries remain tracked: a call at or after a let-destructure (#764), and a call nested inside an effect-operation argument (#776).

Full detail in the CHANGELOG.