fix(802): defer string_length to Tier 3 for UTF-8 byte soundness (v0.0.182)

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.182] - 2026-06-27
+
+### Fixed
+
+- **Verifier soundness: `string_length` no longer proves a false length for non-ASCII strings** (final sub-task of the [#392](https://github.com/aallan/vera/issues/392) `smt.py` soundness audit).  `vera verify` translated `string_length` to Z3's `Length`, which counts Unicode **code points**, but Vera's runtime counts **UTF-8 bytes** — so `ensures(string_length("é") == 1)` verified at Tier 1 while the runtime returns `2`.  `string_length` is now modeled at Tier 1 only for a string **literal** (whose exact byte length is known); on any non-literal argument it defers to a runtime-guarded **Tier 3** obligation (Z3's string theory has no byte-length operator), matching the numeric-cast / quantifier / decimal precedent.  The boolean predicates `string_contains` / `string_starts_with` / `string_ends_with` stay Tier 1 — UTF-8 is self-synchronizing, so a valid substring / prefix / suffix matches at the byte level exactly when it matches at the code-point level — with one further guard: a string literal containing a code point above Z3's string-sort alphabet (> U+2FFFF), or a lone surrogate (U+D800–U+DFFF) with no UTF-8 encoding, also defers to Tier 3 — the Z3 Python binding would otherwise store it as escape text and let the predicates match phantom bytes (and a surrogate has no UTF-8 byte length to take).  This was the last of the six soundness bugs ([#797](https://github.com/aallan/vera/issues/797)–[#802](https://github.com/aallan/vera/issues/802)) found by the [#392](https://github.com/aallan/vera/issues/392) audit, which is now complete.  ([#802](https://github.com/aallan/vera/issues/802))
+
 ## [0.0.181] - 2026-06-27
 
 ### Fixed
@@ -2604,7 +2610,8 @@ Small docs sweep — closes six aging documentation issues in one PR.  No code c
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.0.181...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.182...HEAD
+[0.0.182]: https://github.com/aallan/vera/compare/v0.0.181...v0.0.182
 [0.0.181]: https://github.com/aallan/vera/compare/v0.0.180...v0.0.181
 [0.0.180]: https://github.com/aallan/vera/compare/v0.0.179...v0.0.180
 [0.0.179]: https://github.com/aallan/vera/compare/v0.0.178...v0.0.179

HISTORY.md

@@ -392,6 +392,7 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | v0.0.179 | 26 Jun | **The `smt.py` soundness-audit batch lands: signed `/` and `%` truncate toward zero, a body `assert(P)` carries a Tier-1 obligation (loud `E507`), contract-position divisions get a `div_zero` obligation, and a prior `assert`/`assume` now discharges later obligations plus the postcondition at Tier 1** ([#392](https://github.com/aallan/vera/issues/392)). |
 | v0.0.180 | 26 Jun | **`@Float64` contracts are verified against Z3's IEEE-754 FloatingPoint sort instead of mathematical reals, so Tier-1 proofs respect `NaN`/`Inf`/signed-zero/rounding and `%` (C `fmod`) and match the runtime, so unsound relational / reflexive Float64 contracts are now correctly rejected** ([#797](https://github.com/aallan/vera/issues/797)). |
 | v0.0.181 | 27 Jun | **`@Int` / `@Nat` arithmetic overflow now traps: `+` / `-` / `*` are partial operations carrying an auto-synthesised `int_overflow` obligation, so a result that provably leaves i64 / u64 range is a compile error (E528) and a dynamic one is a runtime-guarded trap, instead of the verifier proving postconditions the two's-complement runtime then violated** ([#798](https://github.com/aallan/vera/issues/798)). |
+| v0.0.182 | 27 Jun | **`string_length` UTF-8 byte soundness defers non-literal `string_length` to Tier 3 and models string literals at their exact byte length, completing the `smt.py` soundness audit** ([#802](https://github.com/aallan/vera/issues/802)). |
 
 ---
 
@@ -407,4 +408,4 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | Spec chapters | 7 | 10 | 11 | 12 | 13 | 13 | 13 | 13 |
 | Code coverage | — | — | — | 90% | 91% | 96% | 96% | 95% |
 
-Total: **1,400+ commits, 181 tagged releases, 77 active development days.**
+Total: **1,400+ commits, 182 tagged releases, 77 active development days.**

README.md

@@ -215,7 +215,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.0.181 — 1,400+ commits, 181 releases, 5,156 tests, 91% code coverage, 93 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.0.182 — 1,400+ commits, 182 releases, 5,173 tests, 91% code coverage, 93 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [13 chapters](spec/).
 

ROADMAP.md

@@ -8,7 +8,7 @@ Priority lives in this file and nowhere else — issues carry kind and area labe
 
 ## Where we are
 
-5,156 tests, 93 conformance programs, 35 examples, 13 spec chapters.
+5,173 tests, 93 conformance programs, 35 examples, 13 spec chapters.
 
 ## The roadmap
 
@@ -20,7 +20,6 @@ The infrastructure that catches the next regression before a user does, plus the
 
 | Issue | What |
 |---|---|
-| [#392](https://github.com/aallan/vera/issues/392) | Audit the `smt.py` Z3 translation layer for soundness — a bug here silently bypasses verification. |
 | [#807](https://github.com/aallan/vera/issues/807) | Tier-1 model the deferred-but-modelable `@Float64` builtins from #797.  **Blocked by #798**: `int_to_float`/`float_to_int` cross the Int↔Float boundary that the unbounded-`Int` idealisation (#798) makes unsound, so they wait on that fix; `float_clamp` is unblocked but needs a verify-vs-run codegen differential first.  The four format/parse builtins (`float_to_string`, `parse_float64`, `decimal_from_float`/`_to_float`) are Tier-3 by necessity, not deferred. |
 | [#808](https://github.com/aallan/vera/issues/808) | Give the `@Int` / `@Nat` arithmetic-overflow runtime trap (#798) a precise `overflow` trap kind, so a dynamic overflow surfaces as a dedicated trap message rather than the generic `unreachable` kind it currently shares. |
 | [#592](https://github.com/aallan/vera/issues/592) | End-to-end behavioural tests for the five UTF-8 decode sites currently pinned only by structural greps. |