pyspec: extend predicate bodies with strict comparisons, equality, and integer arithmetic#1206
Open
julesmt wants to merge 2 commits into
Open
pyspec: extend predicate bodies with strict comparisons, equality, and integer arithmetic#1206julesmt wants to merge 2 commits into
julesmt wants to merge 2 commits into
Conversation
added 2 commits
May 21, 2026 13:02
`transCompare` previously enumerated only `<=` / `>=` for the general
case (with a `subject == "literal"` short-circuit reused as enum
membership). Strict comparisons `<` / `>` and equalities `==` / `!=`
between non-literal operands fell through to `unsupported comparison`,
dropping the obligation silently in lax mode. `makeComparison` also
required at least one literal operand, so var-to-var comparisons like
`x != y` were always rejected.
Adds matching constructors and lowering at every layer:
* SpecExpr.{intGt,intLt,intEq,intNe,floatGt,floatLt,floatEq,floatNe}
+ softBEq arms.
* DDM ops `intGtExpr` / `intLtExpr` / `intEqExpr` / `intNeExpr`
(and float variants), wired through toDDM/fromDDM.
* TypedStmtExpr builders int/real Gt/Lt/Eq/Ne lowering to
`PrimitiveOp .Gt/.Lt/.Eq/.Neq`.
* `Specs/ToLaurel.specExprToLaurel` arms producing the right
`intGt` / `intLt` / `intEq` / `intNe` (and float) calls.
* `transCompare` arms for `.Gt` / `.Lt` / `.Eq` / `.NotEq`, both in
the `len(subject)` short-circuit and in the general type-checked
path via `makeComparison`.
* `makeComparison` extended: when one operand is int- or Any-typed
and the other is a non-literal of compatible type, dispatch to
the int constructor (covers var-to-var, parameter-to-parameter,
and arithmetic-result-to-parameter).
* `isAnyType` helper on `SpecType` (mirrors `isIntType`).
Tests: new `predicate_compare.py` fixture exercises strict `<` `>`,
`==`, `!=` with both literal-bound and var-to-var operands. The
existing `warnings.py` "unsupported comparison" probe is updated to
use a chained comparison (still rejected by `transCompare`'s
`ops.size = 1` guard).
After this commit, `assert x > 0`, `assert result != x`, and similar
shapes translate to a precise SMT obligation rather than a placeholder.
`transExpr` previously hit `unsupported BinOp` for any `+`, `-`, `*`,
`//`, or `%` between integer-typed predicate operands, dropping the
expression to a placeholder. Postcondition shapes like
`assert kw["x"] + kw["y"] >= 0` translated to a vacuous obligation.
Adds matching constructors and lowering at every layer:
* SpecExpr.{intAdd, intSub, intMul, intDiv, intMod} + softBEq arms.
`intDiv` is Python `//` (floor division); `intMod` is `%`.
* DDM ops `intAddExpr` / `intSubExpr` / `intMulExpr` /
`intDivExpr` / `intModExpr`, wired through toDDM/fromDDM.
* TypedStmtExpr builders intAdd/Sub/Mul/FloorDiv/Mod lowering to
`PrimitiveOp .Add/.Sub/.Mul/.Div/.Mod`.
* `Specs/ToLaurel.specExprToLaurel` arms producing the right
`intAdd` / `intSub` / `intMul` / `intFloorDiv` / `intMod` calls.
* `transExpr` `.BinOp` arm: type-checked dispatch to the matching
`SpecExpr` constructor when both operands are int- or Any-typed,
falling back to placeholder with a `specWarning` otherwise.
Tests: new `predicate_arith.py` fixture exercises each operator with
both `kw[…]`-bound and literal operands.
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.
Extends the PySpec predicate-body recognizer (
transExpr/transCompare)so common assertion shapes translate to precise SMT obligations instead
of silently dropping to a placeholder.
Strict comparisons and equality (
<>==!=). The recognizerpreviously enumerated only
<=/>=for the general case (with asubject == "literal"short-circuit reused as enum membership). Allother comparisons fell through to
unsupported comparison. Alsoloosens
makeComparisonso var-to-var comparisons (x != y,x < ybetween two parameters) translate, not just literal-boundones.
Integer arithmetic (
+-*//%).transExprpreviouslyhit
unsupported BinOpfor any arithmetic operator, droppingexpressions like
kw["x"] + kw["y"] >= 0to a placeholder.After this PR, predicates like
assert x > 0,assert result != x,and
assert kw["x"] + kw["y"] >= 0translate end-to-end (PySpec →DDM → Laurel → Core).