Skip to content

0.9.1 — call-site constants and guard inlining

Choose a tag to compare

View all tags
@tiagoschmitt tiagoschmitt released this 19 Aug 04:27
· 11 commits to main since this release
v0.9.1
b9ea5bb

Highlights

Module constants are facts at call sites. 0.9.0 resolved module constants inside function bodies; 0.9.1 extends them to call-site obligations. An argument or guard mentioning a trusted constant pins it to its declared value — order(MIN_QTY) discharges requires(qty >= 10) when const MIN_QTY = 10, and counterexamples stop showing free values for named constants. Locally shadowed names skip the fact.

Method-call guards work as path conditions. Path conditions now inline pure method contracts before translation: if (x.lte(0)) return ...; f(x) discharges f's requires(x.gt(0)). This kills the early-return guard false-positive class for Decimal-style method comparisons at call sites.

🤖 Generated with Claude Code

Assets 2
Loading