pyspec: extend predicate bodies with strict comparisons, equality, and integer arithmetic#1206
pyspec: extend predicate bodies with strict comparisons, equality, and integer arithmetic#1206julesmt wants to merge 7 commits into
Conversation
`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.
| def intMul (x y : TypedStmtExpr .TInt) | ||
| (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt := | ||
| .ofStmt (.PrimitiveOp .Mul [x.stmt, y.stmt]) source | ||
|
|
There was a problem hiding this comment.
The doc-comment is wrong: Python // is floor division (rounds toward −∞), but Laurel PrimitiveOp.Div resolves to Int.ediv (Euclidean — non-negative remainder). They coincide only when the divisor is positive.
Example: -7 // -2 is 3 in Python (floor of 3.5) but 4 in Euclidean (since -7 = -2·4 + 1). Same divergence for intMod at line 110: Python % matches the sign of the divisor, Euclidean mod is always non-negative.
This is pre-existing behavior inherited from Strata/Languages/Python/PythonToCore.lean:180, but predicate bodies will silently produce wrong VCs whenever a divisor can be negative. Two options:
- Tighten the doc-comment to say "matches Python only when the divisor is positive" and file an issue to add a true floor-div op to Laurel/Core.
- Emit a
specWarninginSpecs.lean:952when the divisor sign isn't a positive literal.
Minimum: don't claim the semantics is the same in the doc.
| else if subjType.isAnyType && boundType.isAnyType then | ||
| -- Both sides Any-typed (e.g. two function parameters whose types | ||
| -- aren't seeded). Trust the user and use the int comparison. | ||
| some (intCtor subj bound) |
There was a problem hiding this comment.
Silently defaulting to intCtor when both operands are Any-typed (e.g., two unparameterized callees) is unsound if the actual runtime values are floats — the resulting SMT VC will have the wrong sort. Please add a specWarning here so users see that the recognizer is making a guess:
else if subjType.isAnyType && boundType.isAnyType then
specWarning loc s!"comparison between Any-typed operands; assuming int"
some (intCtor subj bound)Or restrict the relaxation to only ==/!= (where the cross-type case is more obviously a Python error).
| | .BinOp _ left op right => | ||
| let (lhs, lhsTp) ← transExpr left | ||
| let (rhs, rhsTp) ← transExpr right | ||
| let okType (tp : SpecType) : Bool := tp.isIntType || tp.isAnyType |
There was a problem hiding this comment.
Asymmetric coverage: this PR adds int +/-/*////% but no float arithmetic. A predicate assert kw["x"] + kw["y"] >= 0.0 with float-typed operands still drops to placeholder. Either mirror the int branch for floats (the constructors are already in PythonLaurelTypedExpr.lean), or note in the PR description that float arithmetic is deliberately deferred and file a follow-up.
| | floatGt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange) | ||
| | floatLt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange) | ||
| | floatEq (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange) | ||
| | floatNe (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange) |
There was a problem hiding this comment.
Refactor opportunity (out of scope for this PR): each new operator forces synchronized edits in 8 places — SpecExpr constructor, softBEq, DDM op, toDDM, fromDDM, specExprToLaurel, PythonLaurelTypedExpr def, and the recognizer. With 13 cases added here, the boilerplate is already painful and the next operator will be more so.
Worth filing a follow-up to collapse to two parameterized constructors:
| intBinOp (op : IntBinOp) (lhs rhs : SpecExpr) (loc : SourceRange) -- Add/Sub/Mul/Div/Mod
| intCompare (op : IntCmp) (lhs rhs : SpecExpr) (loc : SourceRange) -- Eq/Ne/Lt/Le/Gt/GeA round-trip property (toDDM ∘ fromDDM) e = e becomes a one-liner per family rather than a per-constructor case. The proof obligation pre-/post-refactor is itself a useful regression test.
| throw <| IO.userError s!"Unexpected warnings from predicate_arith.py:{warnStr}" | ||
| | .error e => | ||
| throw <| IO.userError e | ||
|
|
There was a problem hiding this comment.
Both new test cases assert only "no warnings produced". A regression in specExprToLaurel (e.g., wrong constructor, wrong type, swapped operand order) is invisible to these tests. Please add one fixture per family that runs the full pipeline (PySpec → DDM → Laurel → Core) and pins the resulting SMT VC shape — at minimum, an assert kw["x"] + kw["y"] >= 0 whose generated obligation includes (>= (+ x y) 0) (or similar) verified via #guard_msgs. Without this, the round-trip soundness is being checked only by absence of warnings.
Python `//` is floor division (toward -inf) and `%` follows the divisor's sign; Laurel `Div` / `Mod` are Euclidean. They coincide only when the divisor is positive. Tighten the doc-comments and emit a recognizer warning whenever the divisor isn't a positive integer literal, so users notice when the generated VC may diverge from the runtime semantics. Tests: fixture asserts the warning fires for `kw["x"] // kw["y"]`.
When a comparison hits two `Any`-typed operands (e.g. unparameterised callees or TypedDict fields annotated `Any`), the recognizer assumed `int` and silently produced an `intCtor` SpecExpr. If the runtime values are floats the generated SMT VC has the wrong sort. Lift `makeComparison` into `SpecAssertionM` and emit a `specWarning` on the Any/Any branch so users see the assumption. Tests: `compare_any_to_any` fixture pins the new warning.
The previous commits added int `+` / `-` / `*` / `//` / `%` recognition; float arithmetic deliberately falls through. Make that intent explicit: when a `BinOp` has at least one float-typed operand, emit a dedicated warning instead of the generic "BinOp with non-int operand" message. Float arithmetic remains deferred because Laurel `Real` models exact mathematical reals while Python floats are IEEE-754 doubles, so a faithful encoding needs a `Float64` lowering path that doesn't yet exist in `ToLaurel.lean`. Tests: `float_arith_unsupported` fixture pins the new warning so a future change that silently lowers floats into the int branch fails loudly.
Adding 13 hand-written constructors forces synchronized edits across `SpecExpr`, `softBEq`, the DDM op decl, `toDDM`, `fromDDM`, `specExprToLaurel`, `PythonLaurelTypedExpr`, and the recognizer. The right long-term shape is a pair of parameterised `intBinOp` / `intCompare` constructors, but that refactor is out of scope here. Add `testSpecExprDDMRoundTrip` covering every new ctor with asymmetric operands (lhs ≠ rhs) where applicable, so an l/r swap or wrong-DDM-ctor regression in `toDDM` / `fromDDM` is detectable. Promote `DDM.SpecExprDecl.fromDDM` from `private` to `protected` so the test can reach it. Leave a TODO above the ctor list in `Decls.lean` pointing at the parameterised refactor.
The previous tests only asserted "no warnings produced" — a regression in `specExprToLaurel` that swapped operands, picked the wrong constructor, or routed an int op through the float branch would slip through unnoticed. Add VC-shape assertions in `ToLaurelTest.lean` for every new ctor: int comparisons `<`, `>`, `==`, `!=`, int arithmetic `+`, `-`, `*`, `//`, `%`, and a representative float comparison `<`. Each test pins both the runtime conversion (`Any..as_int!` / `Any..as_float!`) and the operator symbol against the formatted Laurel body, with asymmetric operands where applicable so an l/r swap renders visibly. The float case additionally asserts the int conversion is *not* present, catching int/float cross-routing.
2 participants
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).