fix(802): defer string_length to Tier 3 for UTF-8 byte soundness (v0.0.182)#810
Conversation
…0.182)
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 (a false proof for every
non-ASCII string). Final sub-task of the #392 smt.py soundness audit.
string_length is now modeled at Tier 1 only for a string literal (its exact byte
length is known); a non-literal argument 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. The offset-sensitive builtins
(string_slice / string_index_of / string_char_code / string_chars) were never
modeled in Z3 and already defer.
Tests that pinned the old z3.Length Tier-1 behavior are rewritten to the sound
deferral; refinement / E501 / #667 tests that used string_length only as an
example builtin switch to string_starts_with (a still-Tier-1 predicate). New
test_string_length_soundness.py covers the literal byte model, slot deferral,
and predicate soundness; ch04_string_builtins gains a non-ASCII byte-length case.
Closes #802.
Closes #392.
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Run ID: ⛔ Files ignored due to path filters (6)
📒 Files selected for processing (15)
📝 WalkthroughWalkthroughThis PR changes ChangesString length soundness
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related issues
Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #810 +/- ##
=======================================
Coverage 92.03% 92.03%
=======================================
Files 89 89
Lines 26853 26855 +2
Branches 321 321
=======================================
+ Hits 24713 24717 +4
+ Misses 2132 2130 -2
Partials 8 8
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
…runtime/edge tests Adversarial review of #810 found a second Z3-string unsoundness in the same class as #802: Z3's string sort alphabet only reaches U+2FFFF, and the Python binding silently stores any higher code point as the literal's escape string — so string_contains("\u{10FFFF}", "f") proved true at Tier 1 while the runtime returns false. Since this PR closes the #392 smt.py string-soundness audit, fixing it here keeps that close honest. - vera/smt.py: a string literal containing a code point > U+2FFFF defers to Tier 3 (StringVal returns None), so the predicates never match phantom escape bytes. string_length is unaffected (it byte-counts the decoded value, not StringVal), so an astral literal's byte length is still soundly Tier-1. - tests/test_string_length_soundness.py: TestAstralStringLiteral802 (the regression — pre-fix proved the false contract at Tier 1) plus literal-edge coverage (escaped-unicode decode, 4-byte emoji, empty string). - tests/test_codegen.py: a non-ASCII runtime byte-length test (string_length("é") == 2, "😀" == 4) — pins the runtime premise the verifier's byte model relies on, so a codegen regression to code-point counting can't hide behind green verifier-side tests. - spec/06 §6.4.3 + CHANGELOG: note the astral-literal Tier-3 deferral. Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/smt.py (1)
1075-1079: 🩺 Stability & Availability | 🟡 Minor | ⚡ Quick winReject lone surrogate escapes before UTF-8 sizing
vera/smt.py:1075-1079
_decode_string_escapes()accepts\u{D800}-style values, solen(arg_node.value.encode("utf-8"))can raiseUnicodeEncodeErrorinstead of falling back to Tier 3. Reject surrogate code points upstream or handle the encode failure here.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@vera/smt.py` around lines 1075 - 1079, The string_length fast path in `vera.smt` can crash on lone surrogate escapes because `arg_node.value.encode("utf-8")` assumes valid UTF-8. Update the `string_length` handling in the SMT translation logic to either reject surrogate code points before calling `encode` or catch `UnicodeEncodeError` and fall back to the Tier 3 path, using the existing `call`/`arg_node` string-literal branch as the place to make the change.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@tests/test_string_length_soundness.py`:
- Around line 124-132: Add an explicit boundary test around the ord(ch) >
0x2FFFF check in the string length soundness suite: extend
test_four_byte_emoji_literal_byte_length or add a nearby case that verifies both
\u{2FFFF} and \u{30000} so the compiler behavior at the exact cutoff is covered.
Use the existing _verify helper and string_length assertions to ensure \u{2FFFF}
is treated on the lower side and \u{30000} on the higher side, catching any
accidental > versus >= regression.
- Around line 192-206: The astral-literal test only checks that Tier 1 did not
verify, which can still pass if verification fails differently or the obligation
disappears. In test_astral_predicate_not_proved_at_tier1, keep the existing
tier1_verified assertion but also assert _ok(result) and that
result.summary.tier3_runtime is at least 1 so the test explicitly covers the
intended Tier-3 fallback behavior.
---
Outside diff comments:
In `@vera/smt.py`:
- Around line 1075-1079: The string_length fast path in `vera.smt` can crash on
lone surrogate escapes because `arg_node.value.encode("utf-8")` assumes valid
UTF-8. Update the `string_length` handling in the SMT translation logic to
either reject surrogate code points before calling `encode` or catch
`UnicodeEncodeError` and fall back to the Tier 3 path, using the existing
`call`/`arg_node` string-literal branch as the place to make the change.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: c7827713-5433-4a0e-bc61-ad9a8cebf0dd
📒 Files selected for processing (8)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdspec/06-contracts.mdtests/test_codegen.pytests/test_string_length_soundness.pyvera/smt.py
…toff/astral tests (review) CodeRabbit review of #810: - vera/smt.py: a lone surrogate (U+D800..U+DFFF) is not UTF-8-encodable, so the new string_length literal byte-model (value.encode) AND z3.StringVal both crashed `vera verify` with UnicodeEncodeError. Guard both: string_length catches UnicodeEncodeError -> Tier 3; the StringVal literal-deferral now covers surrogates alongside the > U+2FFFF astral cutoff. - tests/test_string_length_soundness.py: a surrogate regression test (no crash, defers), an exact-cutoff boundary test (\u{2FFFF} Tier-1 vs \u{30000} Tier-3, pinning > vs >=), and the astral predicate test reworked to the literal-on-literal form so it asserts the clean Tier-3 fallback (_ok + tier3 >= 1). - spec/06 section 6.4.3 + CHANGELOG: note the surrogate deferral. Note: CR's finding 1 suggested a string_length boundary test, but string_length byte-counts via Python and does not exercise the z3.StringVal cutoff, so the boundary test is on a predicate instead. Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai Good catch — reproduced (it crashed |
|
Tip For best results, initiate chat on the files or code changes.
Catching ✏️ Learnings added
|
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/06-contracts.md`:
- Around line 257-258: The String length/spec paragraph overstates the U+2FFFF
fallback and conflicts with `vera/smt.py` and
`tests/test_string_length_soundness.py`. Update the wording in the string
builtins section so the U+2FFFF cutoff applies only to `z3.StringVal`-based
predicate translation (with lone surrogates still deferring to Tier 3), while
`string_length` on literals remains Tier 1 via byte-counting. Keep the existing
references to `string_length`, `string_contains`, `string_starts_with`,
`string_ends_with`, and `z3.StringVal` to anchor the revised scope.
In `@tests/test_string_length_soundness.py`:
- Around line 243-254: The current assertions in test_string_length_soundness.py
only check that tier3_runtime is reached, which still allows a deferred
verification error; update the soundness checks around _verify for string_length
and string_contains to also assert _ok(length) and _ok(predicate). Keep the
existing Tier-3 fallback assertion, but make the test fail if the verifier
reports an E500/checker error instead of a clean graceful fallback, using the
same length and predicate variables.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 161dfdbf-8c72-49e1-9346-2798caa1e07e
📒 Files selected for processing (7)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdspec/06-contracts.mdtests/test_string_length_soundness.pyvera/smt.py
…r-3 fallback (review) CodeRabbit review of #810: - spec/06 section 6.4.3: the string-length paragraph overstated the U+2FFFF cutoff. It applies only to the z3.StringVal-based predicate translation; string_length byte-counts the decoded literal, so an astral (> U+2FFFF) literal's length stays Tier 1. Reworded to scope the cutoff to the predicates, with the lone surrogate (no UTF-8 encoding) still deferring on both paths. - tests/test_string_length_soundness.py: the surrogate test now also asserts _ok(length) and _ok(predicate), so it fails on an E500 / checker error rather than only requiring tier3_runtime — pinning the graceful fallback, not just any deferral. Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
…s-loop test (review-pr) pr-review-toolkit review of #810 (4 agents — all found the fix sound; 0 critical/important code issues). Addressed the agreed findings: - Doc accuracy: comments / spec / CHANGELOG / test-docstring claimed z3.StringVal "raises" on a lone surrogate. It does not (on z3 4.16 it silently stores the code point's escape text, same as the > U+2FFFF astral case); only string_length's value.encode("utf-8") genuinely raises. Reworded vera/smt.py, spec/06, CHANGELOG, and the surrogate test docstring; fixed the astral escape-text illustration ("\U000xxxxx" -> the actual "\u{...}" form). - tests/test_codegen.py: added a runtime soundness-loop test — a slot-arg string_length contract that `vera verify` DEFERS to Tier 3 is enforced at runtime (ensures(@Int.result == 1) over "é" raises a postcondition violation), closing the "deferral is sound, not merely imprecise" loop the verifier-side tests leave open. No behaviour change (comment / test / doc only). Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
pr-review-toolkit review (4 agents, parallel)Ran a comprehensive review of this PR — code-reviewer, pr-test-analyzer, silent-failure-hunter, comment-analyzer — against head Critical / Important: none. All four agents independently validated the fix as sound:
Addressed (the only findings — doc accuracy + one test), in
No behaviour change in this round. |
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tests/test_string_length_soundness.py (1)
217-236: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winThis boundary test is exercising the
requires(...)fallback, not just thez3.StringValcut-off.The
"\u{30000}"literal inrequires(@String.0== ...)takes the repo’s known untranslatable-literal path beforestring_starts_with(...)becomes the interesting part, sotier3_runtime >= 1can still pass without pinning the> 0x2FFFFpredicate boundary itself. Use literal-on-literal probes for both sides of the cut-off and assert the deferred case stays_ok(...).Suggested fix
- modeled = _verify(""" -public fn f(`@String` -> `@Bool`) - requires(`@String.0` == "\\u{2FFFF}") + modeled = _verify(""" +public fn f(`@Unit` -> `@Bool`) + requires(true) ensures(`@Bool.result` == true) effects(pure) -{ string_starts_with(`@String.0`, "\\u{2FFFF}") } +{ string_starts_with("\\u{2FFFF}", "\\u{2FFFF}") } """) assert _ok(modeled) and modeled.summary.tier3_runtime == 0, ( modeled.summary.tier1_verified, modeled.summary.tier3_runtime, ) deferred = _verify(""" -public fn f(`@String` -> `@Bool`) - requires(`@String.0` == "\\u{30000}") +public fn f(`@Unit` -> `@Bool`) + requires(true) ensures(`@Bool.result` == true) effects(pure) -{ string_starts_with(`@String.0`, "\\u{30000}") } +{ string_starts_with("\\u{30000}", "\\u{30000}") } """) + assert _ok(deferred), [d.description for d in deferred.diagnostics] assert deferred.summary.tier3_runtime >= 1, ( deferred.summary.tier1_verified, deferred.summary.tier3_runtime, )Based on learnings, astral literals inside
requires(...)are dropped as untranslatable in this repo, and as per path instructions this test should pin the exact observable it claims to cover.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_string_length_soundness.py` around lines 217 - 236, The current test in test_string_length_soundness is hitting the untranslatable-literal fallback in requires(...) instead of validating the string boundary in string_starts_with(...). Update the probe to use literal-on-literal checks on both sides of the 0x2FFFF cutoff, and make the deferred case assert _ok(...) with the expected tier3_runtime behavior so the test directly covers the intended boundary rather than the fallback path. Use the existing _verify, _ok, and string_starts_with symbols to keep the assertions focused on the cutoff behavior.Sources: Path instructions, Learnings
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@tests/test_codegen.py`:
- Around line 1239-1243: The test in `test_codegen.py` is too broad because it
accepts raw `wasmtime.Trap`, `WasmtimeError`, and any `RuntimeError`, which can
hide unrelated failures in `execute()`. Narrow the assertion to the
contract-violation wrapper exposed by `vera/codegen/api.py::execute`, and verify
the observable trap shape it normalises to instead of matching generic exception
types. Keep the test focused on the `execute` call with the invalid raw argument
and assert the specific wrapper/error class that represents contract violations.
---
Outside diff comments:
In `@tests/test_string_length_soundness.py`:
- Around line 217-236: The current test in test_string_length_soundness is
hitting the untranslatable-literal fallback in requires(...) instead of
validating the string boundary in string_starts_with(...). Update the probe to
use literal-on-literal checks on both sides of the 0x2FFFF cutoff, and make the
deferred case assert _ok(...) with the expected tier3_runtime behavior so the
test directly covers the intended boundary rather than the fallback path. Use
the existing _verify, _ok, and string_starts_with symbols to keep the assertions
focused on the cutoff behavior.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: b261ff19-6151-4a8c-9540-3dd409c58d5a
📒 Files selected for processing (8)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdspec/06-contracts.mdtests/test_codegen.pytests/test_string_length_soundness.pyvera/smt.py
CodeRabbit review of b350578 (1 inline + 1 outside-diff, both "Functional Correctness | Minor"). Both findings are the same anti-pattern — an assertion satisfiable by something other than its named target — verified valid by reproduction + mutation: - tests/test_codegen.py: the round-5 runtime soundness-loop test used pytest.raises((WasmtimeError, Trap, RuntimeError)). execute() normalises every wasmtime trap into WasmTrapError (a RuntimeError subclass), so the broad form green-passes on any failure — a setup error or a regression that traps for a different reason. Narrowed to raises(WasmTrapError) + assert kind == "contract_violation" (confirmed empirically: a postcondition violation raises exactly this kind). Mutation: asserting the wrong kind flips the test RED. - tests/test_string_length_soundness.py (test_astral_cutoff_boundary): the slot-arg precondition form (a String param compared to an astral literal) produces TWO tier3 obligations — the astral requires literal also defers — so tier3 >= 1 would still pass if only the requires deferred and the body predicate regressed to Tier 1, masking the soundness-critical path. Rewrote to literal-on-literal with a trivial precondition so a SINGLE postcondition obligation is driven solely by the body predicate's astral literal, and added an explicit clean-deferral assertion. Mutation: removing the > 0x2FFFF guard now flips the isolated assertion RED. Test-only, plus the two TESTING.md line counts. No behaviour change. Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai Re: the outside-diff finding on |
|
Tip For best results, initiate chat on the files or code changes.
You're right: with That addresses my concern. ✏️ Learnings added
|
|
@coderabbitai resume |
|
@coderabbitai full review |
✅ Action performedReviews resumed. |
✅ Action performedFull review finished. |
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@TESTING.md`:
- Line 78: Update the TESTING.md table summary for
test_string_length_soundness.py to also mention the astral/surrogate-literal
predicate regression; the current row only describes the string_length
byte-count behavior and Tier 1 predicates. Edit the row text so it references
the astral/surrogate literal path and its Tier 3 deferral, using the existing
test_string_length_soundness.py entry as the anchor.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: bb3cf7ef-55e5-494f-9c17-021c199aef95
📒 Files selected for processing (8)
CHANGELOG.mdREADME.mdROADMAP.mdTESTING.mdspec/06-contracts.mdtests/test_codegen.pytests/test_string_length_soundness.pyvera/smt.py
… row (CodeRabbit) CodeRabbit full review of 2d2db6e flagged that the test_string_length_soundness.py summary row described the string_length byte-count fix and the Tier-1 predicate cases but omitted the astral/surrogate literal predicate path the file also covers (TestAstralStringLiteral802) — which defers to Tier 3 because z3.StringVal cannot model those code points. Appended that clause so the row matches the file's actual coverage. Doc-only. Refs #802, #392. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai full review |
✅ Action performedFull review finished. |
1 participant
Closes #802 — the final sub-task of the #392
smt.pysoundness audit. With this, all six soundness bugs the audit found (#797–#802) are fixed, so this PR also Closes #392.The bug
vera verifytranslatedstring_lengthto Z3'sLength, which counts Unicode code points, but Vera's runtimestring_lengthcounts UTF-8 bytes. They disagree on every multibyte character, so the verifier proved false contracts:vera verify→ proved at Tier 1 (Z3Length("é") == 1), yetvera runraises a postcondition violation (string_length("é")is2). Silent for ASCII (1 byte = 1 code point); wrong for any multibyte character.The fix
string_length(vera/smt.py): modeled at Tier 1 only for a string literal, whose exact UTF-8 byte length is known (string_length("é")now proves== 2, disproves== 1); on any non-literal argument it defers to a runtime-guarded Tier 3 obligation — Z3's string theory has no byte-length operator, so this matches the numeric-cast / quantifier / decimal precedent the audit established. Sound, and it preserves the literal-arg precision the originalz3.Lengthwas added for (with the correct byte count).string_contains/string_starts_with/string_ends_withstay Tier 1 because UTF-8 is self-synchronizing — a valid substring/prefix/suffix matches at the byte level exactly when it matches at the code-point level (verified by a verify↔run differential on non-ASCII inputs). The offset-sensitive builtins (string_slice,string_index_of,string_char_code,string_chars) were never translated to Z3 and already defer to Tier 3.Also found in review — astral-plane string literals (folded in)
The adversarial review of this PR surfaced a second Z3-string unsoundness in the same class, so I fixed it here (this PR closes the #392 audit — shipping a known Z3-string hole would make that close dishonest). Z3's string-sort alphabet only reaches U+2FFFF, and its Python binding silently stores any higher code point as the literal's escape text — so
string_contains("\u{10FFFF}", "f")provedtrueat Tier 1 (matching a phantom escape byte) while the runtime returnsfalse. Reproduced, then fixed invera/smt.py: a string literal containing a code point > U+2FFFF defers to Tier 3 (StringValreturnsNone), so the predicates never match phantom bytes.string_lengthis unaffected (it byte-counts the decoded value, notStringVal). Regression test:TestAstralStringLiteral802. The review also prompted a runtime byte-length test (string_length("é") == 2,"😀" == 4) — pinning the runtime premise the verifier's byte model relies on — and escaped-unicode / 4-byte / empty-literal coverage.Exit checklist (§0)
pytest tests/— green (5,138 passed, 16 skipped, 16 deselected)mypy vera/— cleancheck_conformance.py— 93/93 (ch04_string_builtins.veragains a non-ASCII byte-length case that verifies at Tier 1 and runs as2)check_examples.py— 35/35check_version_sync.py— 0.0.182[0.0.182]+ link refs; doc-counts / site-assets / spec-examples greentests/test_string_length_soundness.py(RED-confirmed: pre-fix proves== 1/ disproves== 2)Tests
tests/test_string_length_soundness.py(8): the literal byte-model ("é"→2, not1), slot-arg deferral (the issue's probe no longer proves at Tier 1), ASCII preservation, and the predicate-soundness guards (verify↔run agree on non-ASCII).TestStringLengthVerificationassertedstring_lengthwas Tier-1 viaz3.Length(it now asserts the deferral / literal byte-model). Refinement, E501-rendering, and Expand smt.translate_expr coverage: FloatLit, ArrayLit, IndexExpr #667 call-typing tests that usedstring_lengthonly as an example builtin switch tostring_starts_with(a still-Tier-1 predicate), preserving each test's actual purpose. The aggregate tier-count test moves -2 T1 / +2 T3 (two example contracts defer), total unchanged.Reproduce-before-fix note (CR's suggested option)
The issue offered a byte-indexed Z3 model as the alternative to deferral. A full byte model would require re-encoding Vera strings as Z3 byte-sequences (
SeqSortofBitVec8) — a large rework that would itself need an audit. The literal-byte-length model here fixes the unsoundness, keeps the documented literal-arg precision, and minimises collateral weakening (sound checks likestring_length("") > 0over a literal still decide statically); a richer byte model can follow if Tier-1 string-length reasoning over variables is ever needed.🤖 Generated with Claude Code
Summary by CodeRabbit
string_lengthby modelling supported string literals using exact UTF-8 byte length; non-literal inputs now defer to runtime-guarded Tier 3 checks, with added safeguards for astral and lone-surrogate edge cases.string_contains,string_starts_with, andstring_ends_withwhere sound, with Tier 3 deferrals for problematic literals.string_lengthsoundness regression suite and updated tiering/verification expectations, including an end-to-end contract-violation case for issue 802.v0.0.182, refreshing documented release and test-status totals.