fix: SMT translator String/Float64 param sorts + string predicates (v0.0.111)#456
Merged
Conversation
string_length() was missing from _translate_call in smt.py, causing requires(string_length(@String.0) > 0) and similar contracts to fall back to Tier 3 runtime checks even though the constraint is trivially decidable. Fix: treat string_length as an uninterpreted function with the axiom result >= 0, matching the pattern used for array_length, map_size, and set_size. The inference.vera example now verifies 4/4 Tier 1 (was 3/4 Tier 1 + 1 Tier 3). Adds TestStringLengthVerification (3 tests) covering: - requires(string_length > 0) → Tier 1 - ensures(@Int.result >= 0) on string_length return → Tier 1 - string_length in comparison expression → Tier 1 Updates tier count baseline: 172 T1 / 19 T3 (was 170 / 21). Co-Authored-By: Claude <noreply@anthropic.invalid>
… predicates
Fixes a class of contracts that silently fell to Tier 3 (runtime check)
despite being statically decidable.
Root cause: verifier.py declared String and Float64 function parameters as
z3.IntSort (the else fallback), so String slot refs had the wrong sort and
z3.Contains/PrefixOf/SuffixOf received Int sorts instead of SeqSort.
Changes:
- verifier.py: add _is_string_type / _is_float64_type helpers; declare
String params/returns via smt.declare_string() (z3.SeqSort) and Float64
via smt.declare_float64() (z3.RealSort)
- smt.py: add StringLit → z3.StringVal() translation so string literals
in contracts are encodable
- smt.py: use z3.Length() for string_length on SeqSort args (instead of
an uninterpreted function) so Z3 can prove string_length("literal") > 0
at call sites; uninterpreted fallback retained for non-string sorts
- smt.py: add string_contains → z3.Contains, string_starts_with →
z3.PrefixOf, string_ends_with → z3.SuffixOf (native string theory)
- smt.py: add explicit return None for float_is_nan / float_is_infinite
with comment explaining why BoolVal(False) would be unsound (Float64 is
modeled as reals; making the check always-False would silently drop the
runtime guard)
test_verifier.py: add TestStringPredicateVerification (5 tests)
- string_contains/starts_with/ends_with → Tier 1
- float_is_nan/float_is_infinite → Tier 3 (correct, preserved)
test_verifier_coverage.py: update 7 tests that used StringLit as
"untranslatable" stand-in; StringLit is now translatable so tests
switch to FloatLit; string equality / string predicate tests updated
from "expects Tier 3" to "expects Tier 1"
Co-Authored-By: Claude <noreply@anthropic.invalid>
Co-Authored-By: Claude <noreply@anthropic.invalid>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughBumps project to v0.0.111 and updates SMT translation and verifier declarations so String and Float64 use correct Z3 sorts; translates string literals to z3.StringVal(), adds native Z3 string ops, and preserves float_is_nan/float_is_infinite as Tier‑3 fallbacks. Changes
Sequence Diagram(s)sequenceDiagram
participant AST as AST / Tests
participant Translator as SMT Translator
participant Verifier as Verifier
participant Z3 as Z3 Solver
Note over AST,Verifier: Old flow (pre-change)
AST->>Translator: emit StringLit / string ops / Float64 param
Translator->>Translator: unsupported or wrong sort → returns None
Translator-->>Verifier: no native Z3 term (Tier 3 fallback)
Note over AST,Verifier: New flow (v0.0.111)
AST->>Translator: StringLit
Translator->>Z3: z3.StringVal(literal)
Z3-->>Translator: String term
AST->>Verifier: declare param/result of type String/Float64
Verifier->>Translator: request declaration
Translator->>Z3: declare SeqSort / Real constant
Z3-->>Verifier: Z3-typed constant
AST->>Translator: string_length / contains / starts_with / ends_with
Translator->>Z3: z3.Length / z3.Contains / z3.PrefixOf / z3.SuffixOf
Z3-->>Translator: Int/Bool terms (Tier 1)
AST->>Translator: float_is_nan / float_is_infinite
Translator->>Translator: return None
Note over Translator: Tier 3 runtime guard preserved
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #456 +/- ##
==========================================
+ Coverage 90.34% 90.35% +0.01%
==========================================
Files 50 50
Lines 19502 19544 +42
Branches 225 225
==========================================
+ Hits 17619 17659 +40
- Misses 1879 1881 +2
Partials 4 4
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@ROADMAP.md`:
- Line 223: Update the outdated release count string "**110 tagged releases**"
in the ROADMAP.md text to "**111 tagged releases**" (the line reading "**630+
commits, 110 tagged releases, 3,247 tests, 96% coverage, 73 conformance
programs, 30 examples, 13 spec chapters.**") so the documented release count
matches v0.0.111; ensure the revised sentence keeps the same formatting and link
to HISTORY.md unchanged.
In `@vera/verifier.py`:
- Around line 460-463: The string/float branch falls through to declare_int when
types are wrapped in RefinedType; update the logic that decides sorts so
RefinedType(String, ...) and RefinedType(Float64, ...) are detected. Either
extend _is_string_type and _is_float64_type to unwrap RefinedType (inspect
param_ty.base or param_ty.type and return True when the inner type is the
primitive) or add explicit checks before the declare_int fallback to detect
RefinedType wrappers and call smt.declare_string(z3_name) or
smt.declare_float64(z3_name) accordingly (referencing _is_string_type,
_is_float64_type, RefinedType, declare_string, declare_float64, and declare_int
to locate the relevant branches).
🪄 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: c43f428e-b3ab-4c5a-9a8f-fca8c04ac2ba
⛔ Files ignored due to path filters (5)
docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**uv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (11)
CHANGELOG.mdHISTORY.mdREADME.mdROADMAP.mdTESTING.mdpyproject.tomltests/test_verifier.pytests/test_verifier_coverage.pyvera/__init__.pyvera/smt.pyvera/verifier.py
…test count to 3,249
_is_string_type and _is_float64_type only checked ty == STRING / ty == FLOAT64,
so a function parameter typed as a refinement of String or Float64 (e.g.
type NonEmptyString = { @string | string_length(@String.0) > 0 }) would fall
through to declare_int (IntSort) instead of declare_string / declare_float64.
This caused string predicates (string_length, string_contains, etc.) to use the
uninterpreted-function fallback rather than Z3 native string theory, producing
spurious Tier 3 downgrades.
Fix matches the existing pattern in _is_nat_type:
return ty == STRING or (isinstance(ty, RefinedType) and ty.base == STRING)
return ty == FLOAT64 or (isinstance(ty, RefinedType) and ty.base == FLOAT64)
Also fix ROADMAP.md release count (110 → 111) and bump test counts from 3,247
to 3,249 across TESTING.md, ROADMAP.md, and README.md.
Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/verifier.py (1)
983-985:⚠️ Potential issue | 🟡 Minor
_is_bool_typedoes not unwrapRefinedType, unlike the other helpers.The new
_is_string_type(line 996) and_is_float64_type(line 1001) both unwrapRefinedTypeto check the base type. Similarly,_is_nat_type(line 980) unwrapsRefinedType. However,_is_bool_typeonly checks for exact equality withBOOL.If a refined Bool type (
RefinedType(BOOL, ...)) is ever used as a parameter or return type, it would fall through todeclare_intinstead ofdeclare_bool.Proposed fix for consistency
`@staticmethod` def _is_bool_type(ty: Type) -> bool: """Check if a type is Bool.""" - return ty == BOOL + return ty == BOOL or (isinstance(ty, RefinedType) and ty.base == BOOL)🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@vera/verifier.py` around lines 983 - 985, The _is_bool_type helper currently compares ty directly to BOOL and must instead unwrap RefinedType like the other helpers; update _is_bool_type to detect if ty is a RefinedType, replace ty with its underlying/base type (as done in _is_string_type/_is_float64_type, e.g., ty = ty.base_type or ty.type depending on your RefinedType field name), then compare the unwrapped ty to BOOL so refined boolean types are recognized as booleans by declare_bool.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Outside diff comments:
In `@vera/verifier.py`:
- Around line 983-985: The _is_bool_type helper currently compares ty directly
to BOOL and must instead unwrap RefinedType like the other helpers; update
_is_bool_type to detect if ty is a RefinedType, replace ty with its
underlying/base type (as done in _is_string_type/_is_float64_type, e.g., ty =
ty.base_type or ty.type depending on your RefinedType field name), then compare
the unwrapped ty to BOOL so refined boolean types are recognized as booleans by
declare_bool.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 882fabaf-7a7c-4b02-8238-d49142d043cd
📒 Files selected for processing (5)
README.mdROADMAP.mdTESTING.mdtests/test_verifier.pyvera/verifier.py
_is_bool_type only checked ty == BOOL, leaving RefinedType(base=BOOL) params falling through to declare_int (IntSort) instead of declare_bool (BoolSort). Fix follows the same pattern as _is_nat_type, _is_string_type, and _is_float64_type: return ty == BOOL or (isinstance(ty, RefinedType) and ty.base == BOOL) Adds test_refined_bool_param_verifies_cleanly to TestRefinedTypeParamSorts. Updates test count from 3,249 to 3,250 across TESTING.md, ROADMAP.md, and README.md. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai Fixed — def _is_bool_type(ty: Type) -> bool:
"""Check if a type is Bool (including refinements of Bool)."""
return ty == BOOL or (isinstance(ty, RefinedType) and ty.base == BOOL)Added |
|
Tip For best results, initiate chat on the files or code changes.
✏️ Learnings added
🧠 Learnings used |
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@tests/test_verifier.py`:
- Around line 1892-1914: The test test_refined_bool_param_verifies_cleanly
currently uses ensures(true) so it doesn't exercise Bool sort handling; update
the contract to be Bool-dependent by replacing ensures(true) with a boolean
assertion that references the parameter (e.g. ensures(`@Flag.0`)) so the verifier
must treat the parameter as Bool, and while here check that RefinedType wrappers
are handled by the verifier helper _is_bool_type (and other primitive-type
helpers) so they recognise RefinedType — adjust the test
(test_refined_bool_param_verifies_cleanly) and/or verifier predicates (e.g.
_is_bool_type in vera/verifier.py) accordingly.
- Around line 1706-1838: Replace the repeated parse_to_ast/typecheck/verify
plumbing in the new tests (e.g., test_string_length_gt_zero_requires_tier1,
test_string_length_ensures_tier1, test_string_length_comparison_tier1,
test_string_contains_tier1, test_string_starts_with_tier1,
test_string_ends_with_tier1, test_float_is_nan_stays_tier3,
test_float_is_infinite_stays_tier3) with the test helpers used across the suite:
call _verify_ok() or _verify_err() (or _check_ok/_check_err where appropriate)
with the source string and then assert against the returned summary, so you
remove the explicit parse_to_ast/typecheck/verify sequence and use
_verify/_verify_ok to maintain consistency and reduce duplication.
🪄 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: d28851c0-36ca-463f-96e2-ae8134cb6ea2
📒 Files selected for processing (5)
README.mdROADMAP.mdTESTING.mdtests/test_verifier.pyvera/verifier.py
… test Replace inline parse_to_ast/typecheck/verify sequences in 11 tests across TestStringLengthVerification, TestStringPredicateVerification, and TestRefinedTypeParamSorts with the existing _verify() helper, removing ~33 lines of duplicated plumbing. Strengthen test_refined_bool_param_verifies_cleanly: replace ensures(true) (vacuous — proves regardless of sort) with requires(@Flag.0)/ensures(@Bool.result) so the test actually exercises BoolSort handling. With IntSort, Z3 cannot treat the parameter as a boolean guard; with BoolSort the contract is Tier 1. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@TESTING.md`:
- Line 9: Update the test totals row in TESTING.md by replacing the outdated
"3,239 passed" with the correct "3,247 passed" and ensure the top-level total
count (the "3,250 across 27 files" number) is reconciled with the PR run output
(adjust the overall total to match passed + skipped if necessary) so the table
reflects "3,247 passed, 11 skipped" exactly.
In `@tests/test_verifier.py`:
- Around line 1703-1704: Update the docstring on class
TestStringLengthVerification to reflect that string_length() for `@String`
arguments uses the native z3.Length(...) translation rather than an
uninterpreted function; mention that uninterpreted functions are only used as a
fallback for non-string sorts so the docstring accurately describes current SMT
behaviour.
🪄 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: e9ad389b-d707-47f1-87d0-16abd535a1c6
📒 Files selected for processing (2)
TESTING.mdtests/test_verifier.py
…eted fn The class docstring said 'via uninterpreted function' but string_length() now uses z3.Length() for SeqSort (String) arguments, giving Z3 full native string theory semantics. The uninterpreted function is only a fallback for non-SeqSort sorts, which is never reached in practice for @string parameters. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
TESTING.md (1)
9-9:⚠️ Potential issue | 🟡 MinorOverview test totals are stale against this PR’s recorded run.
Line 9 still says
3,239 passed, but the PR metadata for this change set reports3,247 passedand11 skipped. Please update the passed count and the aggregate test total so the row remains internally consistent.📝 Proposed fix
-| **Tests** | 3,250 across 27 files (~34,000 lines of test code; 3,239 passed, 11 skipped) | +| **Tests** | 3,258 across 27 files (~34,000 lines of test code; 3,247 passed, 11 skipped) |As per coding guidelines: "
**/*.md: Review Markdown files for factual accuracy against the codebase, broken links, and outdated information."🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@TESTING.md` at line 9, Update the test summary row in TESTING.md to reflect the new counts: change the passed count from 3,239 to 3,247 and the aggregate total from 3,250 to 3,258 (since 3,247 passed + 11 skipped = 3,258), keeping the existing table formatting and the rest of the text intact so the row remains internally consistent.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@tests/test_verifier.py`:
- Around line 1741-1749: The test test_string_length_comparison_tier1 currently
only requires(`@Int.0` >= 0) and ensures(true), so it never exercises the contract
path that calls string_length in the longer_than function; update the test to
assert the actual postcondition by replacing the trivial ensures(true) (or
adding an assertion after invocation) with ensures(string_length(`@String.0`) >
`@Int.0`) or otherwise invoke longer_than in a way that forces evaluation of
string_length so the Tier‑1 encoding is exercised; locate the longer_than
function and the test case name test_string_length_comparison_tier1 to apply
this change.
---
Duplicate comments:
In `@TESTING.md`:
- Line 9: Update the test summary row in TESTING.md to reflect the new counts:
change the passed count from 3,239 to 3,247 and the aggregate total from 3,250
to 3,258 (since 3,247 passed + 11 skipped = 3,258), keeping the existing table
formatting and the rest of the text intact so the row remains internally
consistent.
🪄 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: b92502f7-a726-4f05-a20b-2c35859142a9
📒 Files selected for processing (2)
TESTING.mdtests/test_verifier.py
…ng_length Replace ensures(true) (vacuous) with ensures(string_length(@String.0) >= 0) so string_length is exercised in a contract clause, not just the function body. Z3 proves this via native z3.Length() semantics, giving >=2 Tier 1 contracts. Co-Authored-By: Claude <noreply@anthropic.invalid>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
declare_int()(theelsefallback inverifier.py). String params are now declared viadeclare_string()(Z3 SeqSort) and Float64 viadeclare_float64()(Z3 RealSort). This was the root cause of all the other failures.StringLitnow translates toz3.StringVal()— string literals in contract expressions (e.g.requires(string_starts_with(@String.0, "https://"))) were returningNonefromtranslate_expr, silently demoting contracts to Tier 3.string_lengthusesz3.Length()for String sorts — replaces the uninterpreted function, giving Z3 full semantics sostring_length("literal") > 0is provable at call sites. The uninterpreted fallback is kept for non-string sorts.string_contains,string_starts_with,string_ends_withnow Tier 1 — encoded via Z3 native string theory (z3.Contains,z3.PrefixOf,z3.SuffixOf).float_is_nan/float_is_infiniteexplicitly returnNone— previously fell through silently. Now documented: encoding asBoolVal(False)would be unsound (would drop the runtime guard), so Tier 3 is correct for these.Discovered while running
vera verify examples/inference.veraafter adding Mistral support —requires(string_length(@String.0) > 0)was emitting a Tier 3 warning on working code.Test plan
TestStringLengthVerification(3 tests) —string_lengthcontracts verify Tier 1TestStringPredicateVerification(5 tests) —string_contains/starts_with/ends_withTier 1;float_is_nan/infinitecorrectly Tier 3vera verify examples/inference.vera— now 4/4 Tier 1, no warningsmypy vera/— cleanGenerated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Tests
Chores / Documentation