v0.0.181

[0.0.181] - 2026-06-27

Fixed

• Verifier + codegen soundness: @Int / @Nat arithmetic overflow now traps (batch 4 of the #392 smt.py soundness audit). The verifier modelled @Int / @Nat as Z3's unbounded integers, so + / - / * were total — it proved postconditions the i64 / u64 runtime then violated under two's-complement wraparound: ensures(@Int.result > @Int.0) for { @Int.0 + 1 } verified at Tier 1, yet inc(i64.MAX) wraps to i64.MIN. @Int / @Nat + / - / * are now partial operations that trap on overflow at runtime (consistent with @Nat underflow and signed-division MIN / -1), and the verifier auto-synthesises an int_overflow obligation that the result stays in range — a two-check mirroring array bounds: provably in range → Tier 1; provably out of range (e.g. a literal u64.MAX + 1, or @Int.0 + 1 under requires(@Int.0 == i64.MAX)) → a compile error (E528); dynamic operands → a runtime-guarded Tier-3 overflow trap. Overflow is classified at the operands' common (coerced) type (@Int if either operand is @Int), so a literal-left 5 + @Int.0 and an @Int + 1 narrowed into a @Nat slot are both i64 adds — not the literal's @Nat self-type nor the narrowed result. @Nat subtraction stays the existing underflow obligation (E502). The runtime overflow trap is currently the generic unreachable kind; a precise overflow kind is tracked as #808. (#798)