Fix SMT translation of integer literals#1107
Open
Robertboy18 wants to merge 4 commits intostrata-org:mainfrom
Open
Fix SMT translation of integer literals#1107Robertboy18 wants to merge 4 commits intostrata-org:mainfrom
Robertboy18 wants to merge 4 commits intostrata-org:mainfrom
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
This pull request fixes a type error in the SMT→Lean translation layer by ensuring integer literals are translated with Lean type Int (rather than Prop). This aligns literal typing with translateSort and fixes elaboration failures for integer-valued SMT terms such as ite branches.
Changes:
- Fix
translateTermso.prim (.int x)returns(Int, x)instead of(Prop, x). - Add a regression test exercising an integer-valued SMT
itethat compares against anIntliteral.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
Strata/DL/SMT/Translate.lean |
Corrects the Lean type returned for SMT integer literals during translation (mkInt instead of mkProp). |
StrataTest/DL/SMT/TranslateTests.lean |
Adds a regression test covering an integer-valued ite translated into Lean. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
reviewed
May 5, 2026
tautschnig
added a commit
that referenced
this pull request
May 5, 2026
Addresses the two review comments on PR #1109: 1. `.app .str_length` silently built `Int.ofNat (String.length x)` even when `x` was not a `String`. Check the operand's translated type against `mkString` via a new `expectString` helper (shape mirrors `getBitVecWidth`), so malformed terms throw rather than producing an ill-typed `Expr` that only fails much later. 2. `.app .str_concat` delegated to `leftAssocOp`, which neither rejects fewer-than-two operands (despite its error message claiming it does) nor checks that operands have the expected type. So `.app .str_concat [s]` silently translated to `s`, and a mixed-type list produced an ill-typed `HAppend.hAppend`. Both diverged from `Denote.leftAssoc`. Inline the op instead: require two or more operands explicitly and `expectString` every operand, matching what `Denote.leftAssoc` does for `str_concat`. The underlying `leftAssocOp` bug (silent-singleton) affects every other caller (`.app .add`, `.app .sub`, `.app .mul`, `.app .div`, `.app .mod`, plus the bitvec analogues); it is pre-existing and will be fixed in a separate PR so that the change set can be reviewed on its own merits. Regression tests added in StrataTest/DL/SMT/TranslateTests.lean: - A >2-ary happy-path `str_concat` to cover the foldl tail. - `str_length` applied to a non-string operand. - Singleton `str_concat`. - `str_concat` with a non-string operand in first position. Each error-path test fails on the previous commit (producing the ill-typed `Expr` or the singleton pass-through) and passes here. Tests use `.prim (.bool _)` for the non-string operand so that the expected error message is stable regardless of how `.prim (.int _)` happens to be typed (see PR #1107). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Author
|
I reran all the tests and it all worked! |
tautschnig
approved these changes
May 5, 2026
aqjune-aws
approved these changes
May 5, 2026
Contributor
|
We will have to go through the shepherding process. (https://github.com/strata-org/Strata/blob/main/CONTRIBUTING.md#two-step-review-and-finding-a-shepherd). I will create a separate pull request which will include preserved commits under your email. |
Contributor
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
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.
Issue #, if available:
N/A. Found while working on leanprover/cslib#539.
Description of changes:
This fixes SMT translation of integer literals. Previously,
Strata.DL.SMT.Translate.translateTermtranslated.prim (.int x)as having Lean typeProp; this PR changes it toInt.This matters for integer-valued SMT
iteterms. In CSLib/Boole (Check: leanprover/cslib#539), an expression like:if i + 1 == n then 0 else i + 1was producing a VC elaboration error because the branch literal
0had typeIntbut was expected to have typeProp.This PR also adds a regression test covering an integer-valued SMT
ite.Checks run:
lake env lean StrataTest/DL/SMT/TranslateTests.leanlake env lean StrataTest/DL/SMT/DenoteTests.leanlake env lean StrataTest/DL/SMT/EncoderTests.leanlake build Strata.DL.SMT.Translate StrataTest.DL.SMT.TranslateTestsLet me know if you have any questions!
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.