From 9f4d7b254feb028b27679c92eb3508307ce3b1a8 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Thu, 21 May 2026 12:53:49 -0700
Subject: [PATCH 1/7] pyspec: recognize strict comparison and equality
 operators in predicates

`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.
---
 .../Python/PythonLaurelTypedExpr.lean         | 32 +++++++++++++++
 Strata/Languages/Python/Specs.lean            | 26 ++++++++++--
 Strata/Languages/Python/Specs/DDM.lean        | 32 +++++++++++++++
 Strata/Languages/Python/Specs/Decls.lean      | 18 +++++++++
 Strata/Languages/Python/Specs/ToLaurel.lean   | 40 +++++++++++++++++++
 .../Python/Specs/predicate_compare.py         | 35 ++++++++++++++++
 .../Languages/Python/Specs/warnings.py        |  4 +-
 .../Languages/Python/SpecsTest.lean           | 28 +++++++++++++
 8 files changed, 209 insertions(+), 6 deletions(-)
 create mode 100644 StrataTestExtra/Languages/Python/Specs/predicate_compare.py

diff --git a/Strata/Languages/Python/PythonLaurelTypedExpr.lean b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
index c2b27e09cd..d99bed502a 100644
--- a/Strata/Languages/Python/PythonLaurelTypedExpr.lean
+++ b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
@@ -74,6 +74,22 @@ def intLeq (x y : TypedStmtExpr .TInt)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Leq [x.stmt, y.stmt]) source
 
+def intGt (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Gt [x.stmt, y.stmt]) source
+
+def intLt (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Lt [x.stmt, y.stmt]) source
+
+def intEq (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Eq [x.stmt, y.stmt]) source
+
+def intNe (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Neq [x.stmt, y.stmt]) source
+
 def realGeq (x y : TypedStmtExpr .TReal)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Geq [x.stmt, y.stmt]) source
@@ -82,6 +98,22 @@ def realLeq (x y : TypedStmtExpr .TReal)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Leq [x.stmt, y.stmt]) source
 
+def realGt (x y : TypedStmtExpr .TReal)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Gt [x.stmt, y.stmt]) source
+
+def realLt (x y : TypedStmtExpr .TReal)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Lt [x.stmt, y.stmt]) source
+
+def realEq (x y : TypedStmtExpr .TReal)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Eq [x.stmt, y.stmt]) source
+
+def realNe (x y : TypedStmtExpr .TReal)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
+  .ofStmt (.PrimitiveOp .Neq [x.stmt, y.stmt]) source
+
 def not (x : TypedStmtExpr .TBool)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Not [x.stmt]) source
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 00ec5f786d..6cd98d9b46 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -802,7 +802,10 @@ private def makeComparison
   else if subjType.isIntType then
     match bound with
     | .intLit .. => some (intCtor subj bound)
-    | _ => none
+    | _ =>
+      -- subj is int, bound is int- or Any-typed (a parameter etc.) →
+      -- use the int comparison constructor.
+      if boundType.isIntType || boundType.isAnyType then some (intCtor subj bound) else none
   else if boundType.isFloatType then
     match bound with
     | .floatLit .. => some (floatCtor subj bound)
@@ -810,7 +813,12 @@ private def makeComparison
   else if boundType.isIntType then
     match bound with
     | .intLit .. => some (intCtor subj bound)
-    | _ => none
+    | _ =>
+      if subjType.isIntType || subjType.isAnyType then some (intCtor subj bound) else none
+  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)
   else
     none
 
@@ -825,7 +833,7 @@ private def transCompare (loc : SourceRange)
   let .isTrue h₂ := decideProp (comparators.size = 1)
     | return none
   match lhsExpr with
-  -- len(subject) >= N / len(subject) <= N
+  -- len(subject) >= N / len(subject) <= N / len(subject) > N / len(subject) < N
   | .stringLen _ _ =>
     let (clean, (boundExpr, _)) ← runNoWarn (transExpr comparators[0])
     if clean then
@@ -834,6 +842,8 @@ private def transCompare (loc : SourceRange)
         match ops[0] with
         | .GtE _ => return some (.intGe lhsExpr boundExpr (loc := loc))
         | .LtE _ => return some (.intLe lhsExpr boundExpr (loc := loc))
+        | .Gt _ => return some (.intGt lhsExpr boundExpr (loc := loc))
+        | .Lt _ => return some (.intLt lhsExpr boundExpr (loc := loc))
         | _ => pure ()
       | _ => pure ()
     -- compile("pattern").search(subject) is not None
@@ -852,7 +862,7 @@ private def transCompare (loc : SourceRange)
     | _ => pure ()
   | _ => pure ()
 
-  -- subject >= N / subject <= N (type-checked: int or float)
+  -- subject {>=, <=, >, <, ==, !=} N (type-checked: int or float)
   let (clean, (boundExpr, boundType)) ← runNoWarn (transExpr comparators[0])
   if not clean then
     return none
@@ -862,6 +872,14 @@ private def transCompare (loc : SourceRange)
     return makeComparison (.floatGe · · (loc := loc)) (.intGe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .LtE _ =>
     return makeComparison (.floatLe · · (loc := loc)) (.intLe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .Gt _ =>
+    return makeComparison (.floatGt · · (loc := loc)) (.intGt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .Lt _ =>
+    return makeComparison (.floatLt · · (loc := loc)) (.intLt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .Eq _ =>
+    return makeComparison (.floatEq · · (loc := loc)) (.intEq · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .NotEq _ =>
+    return makeComparison (.floatNe · · (loc := loc)) (.intNe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | _ =>
     return none
 
diff --git a/Strata/Languages/Python/Specs/DDM.lean b/Strata/Languages/Python/Specs/DDM.lean
index 73c1ff245b..ab58bd6927 100644
--- a/Strata/Languages/Python/Specs/DDM.lean
+++ b/Strata/Languages/Python/Specs/DDM.lean
@@ -87,11 +87,27 @@ op intGeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] subject " >=_int " bound;
 op intLeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] subject " <=_int " bound;
+op intGtExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] subject " >_int " bound;
+op intLtExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] subject " <_int " bound;
+op intEqExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] lhs " ==_int " rhs;
+op intNeExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] lhs " !=_int " rhs;
 op floatExpr(value : Str) : SpecExprDecl => value;
 op floatGeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] subject " >=_float " bound;
 op floatLeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] subject " <=_float " bound;
+op floatGtExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] subject " >_float " bound;
+op floatLtExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] subject " <_float " bound;
+op floatEqExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] lhs " ==_float " rhs;
+op floatNeExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(15)] lhs " !=_float " rhs;
 op enumMemberExpr(subject : SpecExprDecl, values : Seq Str) : SpecExprDecl =>
   "enum" "(" subject ", [" values "]" ")";
 op regexMatchExpr(subject : SpecExprDecl, pattern : Str) : SpecExprDecl =>
@@ -275,9 +291,17 @@ protected def SpecExpr.toDDM (e : SpecExpr) : DDM.SpecExprDecl SourceRange :=
   | .intLit v loc => .intExpr loc (toDDMInt loc v)
   | .intGe subj bound loc => .intGeExpr loc subj.toDDM bound.toDDM
   | .intLe subj bound loc => .intLeExpr loc subj.toDDM bound.toDDM
+  | .intGt subj bound loc => .intGtExpr loc subj.toDDM bound.toDDM
+  | .intLt subj bound loc => .intLtExpr loc subj.toDDM bound.toDDM
+  | .intEq l r loc => .intEqExpr loc l.toDDM r.toDDM
+  | .intNe l r loc => .intNeExpr loc l.toDDM r.toDDM
   | .floatLit v loc => .floatExpr loc ⟨loc, v⟩
   | .floatGe subj bound loc => .floatGeExpr loc subj.toDDM bound.toDDM
   | .floatLe subj bound loc => .floatLeExpr loc subj.toDDM bound.toDDM
+  | .floatGt subj bound loc => .floatGtExpr loc subj.toDDM bound.toDDM
+  | .floatLt subj bound loc => .floatLtExpr loc subj.toDDM bound.toDDM
+  | .floatEq l r loc => .floatEqExpr loc l.toDDM r.toDDM
+  | .floatNe l r loc => .floatNeExpr loc l.toDDM r.toDDM
   | .enumMember subj values loc =>
     .enumMemberExpr loc subj.toDDM
       ⟨loc, values.map (⟨loc, ·⟩)⟩
@@ -416,9 +440,17 @@ private def DDM.SpecExprDecl.fromDDM (d : DDM.SpecExprDecl SourceRange) : Specs.
   | .intExpr loc i => .intLit i.ofDDM loc
   | .intGeExpr loc subj bound => .intGe subj.fromDDM bound.fromDDM loc
   | .intLeExpr loc subj bound => .intLe subj.fromDDM bound.fromDDM loc
+  | .intGtExpr loc subj bound => .intGt subj.fromDDM bound.fromDDM loc
+  | .intLtExpr loc subj bound => .intLt subj.fromDDM bound.fromDDM loc
+  | .intEqExpr loc l r => .intEq l.fromDDM r.fromDDM loc
+  | .intNeExpr loc l r => .intNe l.fromDDM r.fromDDM loc
   | .floatExpr loc ⟨_, v⟩ => .floatLit v loc
   | .floatGeExpr loc subj bound => .floatGe subj.fromDDM bound.fromDDM loc
   | .floatLeExpr loc subj bound => .floatLe subj.fromDDM bound.fromDDM loc
+  | .floatGtExpr loc subj bound => .floatGt subj.fromDDM bound.fromDDM loc
+  | .floatLtExpr loc subj bound => .floatLt subj.fromDDM bound.fromDDM loc
+  | .floatEqExpr loc l r => .floatEq l.fromDDM r.fromDDM loc
+  | .floatNeExpr loc l r => .floatNe l.fromDDM r.fromDDM loc
   | .enumMemberExpr loc subj ⟨_, values⟩ => .enumMember subj.fromDDM (values.map (·.2)) loc
   | .regexMatchExpr loc subj ⟨_, pattern⟩ => .regexMatch subj.fromDDM pattern loc
   | .containsKeyExpr loc container ⟨_, key⟩ => .containsKey container.fromDDM key loc
diff --git a/Strata/Languages/Python/Specs/Decls.lean b/Strata/Languages/Python/Specs/Decls.lean
index 21e2bc03c8..d59c93e2f1 100644
--- a/Strata/Languages/Python/Specs/Decls.lean
+++ b/Strata/Languages/Python/Specs/Decls.lean
@@ -387,6 +387,8 @@ def asIdent (tp : SpecType) : Option PythonIdent := do
 
 def isIntType (tp : SpecType) : Bool := tp.asIdent == some .builtinsInt
 
+def isAnyType (tp : SpecType) : Bool := tp.asIdent == some .typingAny
+
 def isFloatType (tp : SpecType) : Bool := tp.asIdent == some .builtinsFloat
 
 def isStringType (tp : SpecType) : Bool := tp.asIdent == some .builtinsStr
@@ -488,10 +490,18 @@ inductive SpecExpr where
 | intLit (value : Int) (loc : SourceRange)
 | intGe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
 | intLe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
+| intGt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
+| intLt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
+| intEq (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange)
+| intNe (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange)
 /-- A floating-point literal, stored as a string to preserve precision. -/
 | floatLit (value : String) (loc : SourceRange)
 | floatGe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
 | floatLe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
+| 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)
 | enumMember (subject : SpecExpr) (values : Array String) (loc : SourceRange)
 /-- `regexMatch subject pattern` asserts that `subject` matches the regular
     expression `pattern`. Corresponds to `compile(pattern).search(subject) is not None`
@@ -525,9 +535,17 @@ def SpecExpr.softBEq : SpecExpr → SpecExpr → Bool
   | .intLit v₁ _, .intLit v₂ _ => v₁ == v₂
   | .intGe s₁ b₁ _, .intGe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
   | .intLe s₁ b₁ _, .intLe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .intGt s₁ b₁ _, .intGt s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .intLt s₁ b₁ _, .intLt s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .intEq a₁ b₁ _, .intEq a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intNe a₁ b₁ _, .intNe a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
   | .floatLit v₁ _, .floatLit v₂ _ => v₁ == v₂
   | .floatGe s₁ b₁ _, .floatGe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
   | .floatLe s₁ b₁ _, .floatLe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .floatGt s₁ b₁ _, .floatGt s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .floatLt s₁ b₁ _, .floatLt s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
+  | .floatEq a₁ b₁ _, .floatEq a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .floatNe a₁ b₁ _, .floatNe a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
   | .enumMember s₁ v₁ _, .enumMember s₂ v₂ _ => s₁.softBEq s₂ && v₁ == v₂
   | .regexMatch s₁ p₁ _, .regexMatch s₂ p₂ _ => s₁.softBEq s₂ && p₁ == p₂
   | .containsKey c₁ k₁ _, .containsKey c₂ k₂ _ => c₁.softBEq c₂ && k₁ == k₂
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index da75cc4076..447103664e 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -340,6 +340,26 @@ def specExprToLaurel (e : SpecExpr) (source : Option FileRange)
     let s ← asAny loc <| specExprToLaurel subject src
     let b ← asAny loc <| specExprToLaurel bound src
     return .mkSome <| .intLeq (.anyAsInt s) (.anyAsInt b)
+  | .intGt subject bound loc => do
+    let src ← nodeSource loc
+    let s ← asAny loc <| specExprToLaurel subject src
+    let b ← asAny loc <| specExprToLaurel bound src
+    return .mkSome <| .intGt (.anyAsInt s) (.anyAsInt b)
+  | .intLt subject bound loc => do
+    let src ← nodeSource loc
+    let s ← asAny loc <| specExprToLaurel subject src
+    let b ← asAny loc <| specExprToLaurel bound src
+    return .mkSome <| .intLt (.anyAsInt s) (.anyAsInt b)
+  | .intEq lhs rhs loc => do
+    let src ← nodeSource loc
+    let l ← asAny loc <| specExprToLaurel lhs src
+    let r ← asAny loc <| specExprToLaurel rhs src
+    return .mkSome <| .intEq (.anyAsInt l) (.anyAsInt r)
+  | .intNe lhs rhs loc => do
+    let src ← nodeSource loc
+    let l ← asAny loc <| specExprToLaurel lhs src
+    let r ← asAny loc <| specExprToLaurel rhs src
+    return .mkSome <| .intNe (.anyAsInt l) (.anyAsInt r)
   | .floatGe subject bound loc => do
     let src ← nodeSource loc
     let s ← asAny loc <| specExprToLaurel subject src
@@ -350,6 +370,26 @@ def specExprToLaurel (e : SpecExpr) (source : Option FileRange)
     let s ← asAny loc <| specExprToLaurel subject src
     let b ← asAny loc <| specExprToLaurel bound src
     return .mkSome <| .realLeq (.anyAsFloat s) (.anyAsFloat b)
+  | .floatGt subject bound loc => do
+    let src ← nodeSource loc
+    let s ← asAny loc <| specExprToLaurel subject src
+    let b ← asAny loc <| specExprToLaurel bound src
+    return .mkSome <| .realGt (.anyAsFloat s) (.anyAsFloat b)
+  | .floatLt subject bound loc => do
+    let src ← nodeSource loc
+    let s ← asAny loc <| specExprToLaurel subject src
+    let b ← asAny loc <| specExprToLaurel bound src
+    return .mkSome <| .realLt (.anyAsFloat s) (.anyAsFloat b)
+  | .floatEq lhs rhs loc => do
+    let src ← nodeSource loc
+    let l ← asAny loc <| specExprToLaurel lhs src
+    let r ← asAny loc <| specExprToLaurel rhs src
+    return .mkSome <| .realEq (.anyAsFloat l) (.anyAsFloat r)
+  | .floatNe lhs rhs loc => do
+    let src ← nodeSource loc
+    let l ← asAny loc <| specExprToLaurel lhs src
+    let r ← asAny loc <| specExprToLaurel rhs src
+    return .mkSome <| .realNe (.anyAsFloat l) (.anyAsFloat r)
   | .not inner loc => do
     let src ← nodeSource loc
     let i ← asBool loc <| specExprToLaurel inner src
diff --git a/StrataTestExtra/Languages/Python/Specs/predicate_compare.py b/StrataTestExtra/Languages/Python/Specs/predicate_compare.py
new file mode 100644
index 0000000000..83815e2cec
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Specs/predicate_compare.py
@@ -0,0 +1,35 @@
+# Fixtures exercising strict comparisons (`<` `>`) and equality
+# (`==` `!=`) between integer-typed predicate operands.
+#
+# Each function uses kwargs typed via a TypedDict so the recognizer
+# knows the operand types. Successful translation produces zero
+# warnings; SpecsTest's predicateCompareTestCase asserts exactly that.
+
+from typing import Unpack, TypedDict
+
+
+Args = TypedDict("Args", {"x": int, "y": int})
+
+
+def strict_lt(**kw: Unpack[Args]) -> None:
+    assert kw["x"] < 10, "x < 10"
+
+
+def strict_gt(**kw: Unpack[Args]) -> None:
+    assert kw["x"] > 0, "x > 0"
+
+
+def equality_with_literal(**kw: Unpack[Args]) -> None:
+    assert kw["x"] == 0, "x == 0"
+
+
+def inequality_var_to_var(**kw: Unpack[Args]) -> None:
+    assert kw["x"] != kw["y"], "x != y"
+
+
+def equality_var_to_var(**kw: Unpack[Args]) -> None:
+    assert kw["x"] == kw["y"], "x == y"
+
+
+def strict_lt_var_to_var(**kw: Unpack[Args]) -> None:
+    assert kw["x"] < kw["y"], "x < y"
diff --git a/StrataTestExtra/Languages/Python/Specs/warnings.py b/StrataTestExtra/Languages/Python/Specs/warnings.py
index e93fa6d089..3c0dac6863 100644
--- a/StrataTestExtra/Languages/Python/Specs/warnings.py
+++ b/StrataTestExtra/Languages/Python/Specs/warnings.py
@@ -1,8 +1,8 @@
 from typing import Any, Dict, List, NotRequired, TypedDict, Unpack
 
-# Unsupported assert pattern: equality comparison
+# Unsupported assert pattern: chained comparison (more than one operator)
 def unsupported_assert(**kw: int) -> None:
-    assert kw["x"] == 1, 'x must be 1'
+    assert 0 <= kw["x"] <= 10, '0 <= x <= 10'
 
 # Unsupported __init__ assignment value (not self._ClassName() pattern)
 class BadInit:
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index ff67b38e92..7ad77c6e37 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -292,6 +292,34 @@ meta def warningTestCase : IO Unit := withPython fun pythonCmd => do
 #guard_msgs in
 #eval warningTestCase
 
+/-- Test that the new strict comparison and equality shapes (`<`, `>`,
+    `==`, `!=`) translate cleanly, both with literal bounds and
+    between two integer-typed operands. -/
+meta def predicateCompareTestCase : IO Unit := withPython fun pythonCmd => do
+  IO.FS.withTempFile fun _handle dialectFile => do
+    IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon
+    IO.FS.withTempDir fun strataDir => do
+      let r ←
+        translateFile
+          (pythonCmd := toString pythonCmd)
+          (dialectFile := dialectFile)
+          (strataDir := strataDir)
+          (pythonFile := testDir / "predicate_compare.py")
+          (searchPath := testDir)
+          |>.toBaseIO
+      match r with
+      | .ok (sigs, warnings) =>
+        if sigs.isEmpty then
+          throw <| IO.userError "Expected signatures from predicate_compare.py but got none"
+        if !warnings.isEmpty then
+          let warnStr := warnings.foldl (init := "") fun acc w => s!"{acc}\n  {w}"
+          throw <| IO.userError s!"Unexpected warnings from predicate_compare.py:{warnStr}"
+      | .error e =>
+        throw <| IO.userError e
+
+#guard_msgs in
+#eval predicateCompareTestCase
+
 
 meta def testNegRoundTrip (v : Nat) : Bool :=
   DDM.Int.ofDDM (.negInt SourceRange.none ⟨.none, v⟩) = .negOfNat v

From d3e5b3b955d86248fb0a160ace3f89ee5880160d Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Thu, 21 May 2026 13:04:18 -0700
Subject: [PATCH 2/7] pyspec: recognize integer arithmetic in predicate bodies
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`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.
---
 .../Python/PythonLaurelTypedExpr.lean         | 23 ++++++++++++++
 Strata/Languages/Python/Specs.lean            | 23 ++++++++++++++
 Strata/Languages/Python/Specs/DDM.lean        | 20 ++++++++++++
 Strata/Languages/Python/Specs/Decls.lean      | 12 +++++++
 Strata/Languages/Python/Specs/ToLaurel.lean   | 25 +++++++++++++++
 .../Languages/Python/Specs/predicate_arith.py | 31 +++++++++++++++++++
 .../Languages/Python/SpecsTest.lean           | 27 ++++++++++++++++
 7 files changed, 161 insertions(+)
 create mode 100644 StrataTestExtra/Languages/Python/Specs/predicate_arith.py

diff --git a/Strata/Languages/Python/PythonLaurelTypedExpr.lean b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
index d99bed502a..9d8da6f91c 100644
--- a/Strata/Languages/Python/PythonLaurelTypedExpr.lean
+++ b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
@@ -90,6 +90,29 @@ def intNe (x y : TypedStmtExpr .TInt)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Neq [x.stmt, y.stmt]) source
 
+def intAdd (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
+  .ofStmt (.PrimitiveOp .Add [x.stmt, y.stmt]) source
+
+def intSub (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
+  .ofStmt (.PrimitiveOp .Sub [x.stmt, y.stmt]) source
+
+def intMul (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
+  .ofStmt (.PrimitiveOp .Mul [x.stmt, y.stmt]) source
+
+/-- Python `//` is floor (Euclidean) division → Laurel `Div`. -/
+def intFloorDiv (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
+  .ofStmt (.PrimitiveOp .Div [x.stmt, y.stmt]) source
+
+/-- Python `%` is Euclidean modulus → Laurel `Mod`. -/
+def intMod (x y : TypedStmtExpr .TInt)
+    (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
+  .ofStmt (.PrimitiveOp .Mod [x.stmt, y.stmt]) source
+
+
 def realGeq (x y : TypedStmtExpr .TReal)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Geq [x.stmt, y.stmt]) source
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 6cd98d9b46..91998ddf6e 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -934,6 +934,29 @@ partial def transExpr (e : expr SourceRange)
     return (.intLit (Int.negOfNat n) (loc := loc), intType)
   | .UnaryOp _ (.USub _) (.Constant _ (.ConFloat _ ⟨_, s⟩) _) =>
     return (.floatLit s!"-{s}" (loc := loc), floatType)
+  -- Integer arithmetic in predicate bodies. Both sides must translate
+  -- cleanly to int-typed (or Any-typed, e.g. function parameters whose
+  -- types weren't seeded into `localTypes`) SpecExprs; the result is
+  -- int-typed. Anything other than int / Any (float, str, …) falls
+  -- through to placeholder so transExpr doesn't claim a type it can't
+  -- justify.
+  | .BinOp _ left op right =>
+    let (lhs, lhsTp) ← transExpr left
+    let (rhs, rhsTp) ← transExpr right
+    let okType (tp : SpecType) : Bool := tp.isIntType || tp.isAnyType
+    if okType lhsTp && okType rhsTp then
+      match op with
+      | .Add _ => return (.intAdd lhs rhs (loc := loc), intType)
+      | .Sub _ => return (.intSub lhs rhs (loc := loc), intType)
+      | .Mult _ => return (.intMul lhs rhs (loc := loc), intType)
+      | .FloorDiv _ => return (.intDiv lhs rhs (loc := loc), intType)
+      | .Mod _ => return (.intMod lhs rhs (loc := loc), intType)
+      | _ =>
+        specWarning loc s!"unsupported BinOp in predicate: {repr op}"
+        return placeholder
+    else
+      specWarning loc s!"BinOp with non-int operand: lhs={repr lhsTp}, rhs={repr rhsTp}"
+      return placeholder
   -- String literal (extract value for use in messages)
   | .Constant _ (.ConString _ ⟨_, _s⟩) _ =>
     return (.placeholder (loc := loc), SpecType.ident loc .builtinsStr)
diff --git a/Strata/Languages/Python/Specs/DDM.lean b/Strata/Languages/Python/Specs/DDM.lean
index ab58bd6927..54b88e9cc9 100644
--- a/Strata/Languages/Python/Specs/DDM.lean
+++ b/Strata/Languages/Python/Specs/DDM.lean
@@ -95,6 +95,16 @@ op intEqExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] lhs " ==_int " rhs;
 op intNeExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] lhs " !=_int " rhs;
+op intAddExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(20), leftassoc] lhs " +_int " rhs;
+op intSubExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(20), leftassoc] lhs " -_int " rhs;
+op intMulExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(25), leftassoc] lhs " *_int " rhs;
+op intDivExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(25), leftassoc] lhs " //_int " rhs;
+op intModExpr(lhs : SpecExprDecl, rhs : SpecExprDecl) : SpecExprDecl =>
+  @[prec(25), leftassoc] lhs " %_int " rhs;
 op floatExpr(value : Str) : SpecExprDecl => value;
 op floatGeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl =>
   @[prec(15)] subject " >=_float " bound;
@@ -295,6 +305,11 @@ protected def SpecExpr.toDDM (e : SpecExpr) : DDM.SpecExprDecl SourceRange :=
   | .intLt subj bound loc => .intLtExpr loc subj.toDDM bound.toDDM
   | .intEq l r loc => .intEqExpr loc l.toDDM r.toDDM
   | .intNe l r loc => .intNeExpr loc l.toDDM r.toDDM
+  | .intAdd l r loc => .intAddExpr loc l.toDDM r.toDDM
+  | .intSub l r loc => .intSubExpr loc l.toDDM r.toDDM
+  | .intMul l r loc => .intMulExpr loc l.toDDM r.toDDM
+  | .intDiv l r loc => .intDivExpr loc l.toDDM r.toDDM
+  | .intMod l r loc => .intModExpr loc l.toDDM r.toDDM
   | .floatLit v loc => .floatExpr loc ⟨loc, v⟩
   | .floatGe subj bound loc => .floatGeExpr loc subj.toDDM bound.toDDM
   | .floatLe subj bound loc => .floatLeExpr loc subj.toDDM bound.toDDM
@@ -444,6 +459,11 @@ private def DDM.SpecExprDecl.fromDDM (d : DDM.SpecExprDecl SourceRange) : Specs.
   | .intLtExpr loc subj bound => .intLt subj.fromDDM bound.fromDDM loc
   | .intEqExpr loc l r => .intEq l.fromDDM r.fromDDM loc
   | .intNeExpr loc l r => .intNe l.fromDDM r.fromDDM loc
+  | .intAddExpr loc l r => .intAdd l.fromDDM r.fromDDM loc
+  | .intSubExpr loc l r => .intSub l.fromDDM r.fromDDM loc
+  | .intMulExpr loc l r => .intMul l.fromDDM r.fromDDM loc
+  | .intDivExpr loc l r => .intDiv l.fromDDM r.fromDDM loc
+  | .intModExpr loc l r => .intMod l.fromDDM r.fromDDM loc
   | .floatExpr loc ⟨_, v⟩ => .floatLit v loc
   | .floatGeExpr loc subj bound => .floatGe subj.fromDDM bound.fromDDM loc
   | .floatLeExpr loc subj bound => .floatLe subj.fromDDM bound.fromDDM loc
diff --git a/Strata/Languages/Python/Specs/Decls.lean b/Strata/Languages/Python/Specs/Decls.lean
index d59c93e2f1..b73023bdb6 100644
--- a/Strata/Languages/Python/Specs/Decls.lean
+++ b/Strata/Languages/Python/Specs/Decls.lean
@@ -494,6 +494,13 @@ inductive SpecExpr where
 | intLt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
 | intEq (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange)
 | intNe (lhs : SpecExpr) (rhs : SpecExpr) (loc : SourceRange)
+| intAdd (lhs rhs : SpecExpr) (loc : SourceRange)
+| intSub (lhs rhs : SpecExpr) (loc : SourceRange)
+| intMul (lhs rhs : SpecExpr) (loc : SourceRange)
+/-- Python `//` (floor division). -/
+| intDiv (lhs rhs : SpecExpr) (loc : SourceRange)
+/-- Python `%` (modulus). -/
+| intMod (lhs rhs : SpecExpr) (loc : SourceRange)
 /-- A floating-point literal, stored as a string to preserve precision. -/
 | floatLit (value : String) (loc : SourceRange)
 | floatGe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
@@ -539,6 +546,11 @@ def SpecExpr.softBEq : SpecExpr → SpecExpr → Bool
   | .intLt s₁ b₁ _, .intLt s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
   | .intEq a₁ b₁ _, .intEq a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
   | .intNe a₁ b₁ _, .intNe a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intAdd a₁ b₁ _, .intAdd a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intSub a₁ b₁ _, .intSub a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intMul a₁ b₁ _, .intMul a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intDiv a₁ b₁ _, .intDiv a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
+  | .intMod a₁ b₁ _, .intMod a₂ b₂ _ => a₁.softBEq a₂ && b₁.softBEq b₂
   | .floatLit v₁ _, .floatLit v₂ _ => v₁ == v₂
   | .floatGe s₁ b₁ _, .floatGe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
   | .floatLe s₁ b₁ _, .floatLe s₂ b₂ _ => s₁.softBEq s₂ && b₁.softBEq b₂
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index 447103664e..7afed627ad 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -360,6 +360,31 @@ def specExprToLaurel (e : SpecExpr) (source : Option FileRange)
     let l ← asAny loc <| specExprToLaurel lhs src
     let r ← asAny loc <| specExprToLaurel rhs src
     return .mkSome <| .intNe (.anyAsInt l) (.anyAsInt r)
+  | .intAdd l r loc => do
+    let src ← nodeSource loc
+    let lv ← asAny loc <| specExprToLaurel l src
+    let rv ← asAny loc <| specExprToLaurel r src
+    return .mkSome <| .fromInt (.intAdd (.anyAsInt lv) (.anyAsInt rv))
+  | .intSub l r loc => do
+    let src ← nodeSource loc
+    let lv ← asAny loc <| specExprToLaurel l src
+    let rv ← asAny loc <| specExprToLaurel r src
+    return .mkSome <| .fromInt (.intSub (.anyAsInt lv) (.anyAsInt rv))
+  | .intMul l r loc => do
+    let src ← nodeSource loc
+    let lv ← asAny loc <| specExprToLaurel l src
+    let rv ← asAny loc <| specExprToLaurel r src
+    return .mkSome <| .fromInt (.intMul (.anyAsInt lv) (.anyAsInt rv))
+  | .intDiv l r loc => do
+    let src ← nodeSource loc
+    let lv ← asAny loc <| specExprToLaurel l src
+    let rv ← asAny loc <| specExprToLaurel r src
+    return .mkSome <| .fromInt (.intFloorDiv (.anyAsInt lv) (.anyAsInt rv))
+  | .intMod l r loc => do
+    let src ← nodeSource loc
+    let lv ← asAny loc <| specExprToLaurel l src
+    let rv ← asAny loc <| specExprToLaurel r src
+    return .mkSome <| .fromInt (.intMod (.anyAsInt lv) (.anyAsInt rv))
   | .floatGe subject bound loc => do
     let src ← nodeSource loc
     let s ← asAny loc <| specExprToLaurel subject src
diff --git a/StrataTestExtra/Languages/Python/Specs/predicate_arith.py b/StrataTestExtra/Languages/Python/Specs/predicate_arith.py
new file mode 100644
index 0000000000..dadd785168
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Specs/predicate_arith.py
@@ -0,0 +1,31 @@
+# Fixtures exercising integer arithmetic (`+`, `-`, `*`, `//`, `%`)
+# inside predicate bodies.
+#
+# Each function uses kwargs typed via a TypedDict so the recognizer
+# knows the operand types. Successful translation produces zero
+# warnings; SpecsTest's predicateArithTestCase asserts exactly that.
+
+from typing import Unpack, TypedDict
+
+
+Args = TypedDict("Args", {"x": int, "y": int})
+
+
+def arith_add(**kw: Unpack[Args]) -> None:
+    assert kw["x"] + kw["y"] >= 0, "x + y >= 0"
+
+
+def arith_sub(**kw: Unpack[Args]) -> None:
+    assert kw["x"] - kw["y"] <= 100, "x - y <= 100"
+
+
+def arith_mul_const(**kw: Unpack[Args]) -> None:
+    assert kw["x"] * 2 >= kw["y"], "x * 2 >= y"
+
+
+def arith_floordiv(**kw: Unpack[Args]) -> None:
+    assert kw["x"] // 2 < kw["y"], "x // 2 < y"
+
+
+def arith_mod(**kw: Unpack[Args]) -> None:
+    assert kw["x"] % 10 == 0, "x % 10 == 0"
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index 7ad77c6e37..440172eb93 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -320,6 +320,33 @@ meta def predicateCompareTestCase : IO Unit := withPython fun pythonCmd => do
 #guard_msgs in
 #eval predicateCompareTestCase
 
+/-- Test that integer arithmetic operators (`+`, `-`, `*`, `//`, `%`)
+    inside predicate bodies translate cleanly. -/
+meta def predicateArithTestCase : IO Unit := withPython fun pythonCmd => do
+  IO.FS.withTempFile fun _handle dialectFile => do
+    IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon
+    IO.FS.withTempDir fun strataDir => do
+      let r ←
+        translateFile
+          (pythonCmd := toString pythonCmd)
+          (dialectFile := dialectFile)
+          (strataDir := strataDir)
+          (pythonFile := testDir / "predicate_arith.py")
+          (searchPath := testDir)
+          |>.toBaseIO
+      match r with
+      | .ok (sigs, warnings) =>
+        if sigs.isEmpty then
+          throw <| IO.userError "Expected signatures from predicate_arith.py but got none"
+        if !warnings.isEmpty then
+          let warnStr := warnings.foldl (init := "") fun acc w => s!"{acc}\n  {w}"
+          throw <| IO.userError s!"Unexpected warnings from predicate_arith.py:{warnStr}"
+      | .error e =>
+        throw <| IO.userError e
+
+#guard_msgs in
+#eval predicateArithTestCase
+
 
 meta def testNegRoundTrip (v : Nat) : Bool :=
   DDM.Int.ofDDM (.negInt SourceRange.none ⟨.none, v⟩) = .negOfNat v

From ef0df5a87b70b25b0598181b4c43e3478bfe9e3d Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 13:27:36 -0700
Subject: [PATCH 3/7] pyspec: warn when `//` / `%` divisor sign isn't
 statically positive

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"]`.
---
 .../Python/PythonLaurelTypedExpr.lean         | 13 +++++++++++--
 Strata/Languages/Python/Specs.lean            | 19 +++++++++++++++++--
 .../Languages/Python/Specs/warnings.py        |  8 ++++++++
 .../Languages/Python/SpecsTest.lean           |  5 +++--
 4 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/Strata/Languages/Python/PythonLaurelTypedExpr.lean b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
index 9d8da6f91c..8f929957d8 100644
--- a/Strata/Languages/Python/PythonLaurelTypedExpr.lean
+++ b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
@@ -102,12 +102,21 @@ def intMul (x y : TypedStmtExpr .TInt)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
   .ofStmt (.PrimitiveOp .Mul [x.stmt, y.stmt]) source
 
-/-- Python `//` is floor (Euclidean) division → Laurel `Div`. -/
+/-- Lowers Python `//` to Laurel `Div`. Laurel `Div` is Euclidean
+    division (`Int.ediv`, non-negative remainder); Python `//` is floor
+    division (rounds toward `-∞`). The two coincide only when the
+    divisor is positive — e.g. `-7 // -2` is `3` in Python but `4` in
+    Euclidean. The recognizer in `Specs.lean` emits a warning when the
+    divisor's sign cannot be proven positive. -/
 def intFloorDiv (x y : TypedStmtExpr .TInt)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
   .ofStmt (.PrimitiveOp .Div [x.stmt, y.stmt]) source
 
-/-- Python `%` is Euclidean modulus → Laurel `Mod`. -/
+/-- Lowers Python `%` to Laurel `Mod`. Laurel `Mod` is Euclidean
+    modulus (always non-negative); Python `%` matches the sign of the
+    divisor. They coincide only when the divisor is positive. The
+    recognizer in `Specs.lean` emits a warning when the divisor's sign
+    cannot be proven positive. -/
 def intMod (x y : TypedStmtExpr .TInt)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TInt :=
   .ofStmt (.PrimitiveOp .Mod [x.stmt, y.stmt]) source
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 91998ddf6e..e655f1ae83 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -944,13 +944,28 @@ partial def transExpr (e : expr SourceRange)
     let (lhs, lhsTp) ← transExpr left
     let (rhs, rhsTp) ← transExpr right
     let okType (tp : SpecType) : Bool := tp.isIntType || tp.isAnyType
+    -- Python `//` and `%` round toward `-∞` and follow the divisor's
+    -- sign respectively; Laurel `Div`/`Mod` are Euclidean. The two
+    -- agree only when the divisor is positive, which we can confirm
+    -- statically just for positive integer literals.
+    let divisorPositive : Bool := match rhs with
+      | .intLit v _ => v > 0
+      | _ => false
     if okType lhsTp && okType rhsTp then
       match op with
       | .Add _ => return (.intAdd lhs rhs (loc := loc), intType)
       | .Sub _ => return (.intSub lhs rhs (loc := loc), intType)
       | .Mult _ => return (.intMul lhs rhs (loc := loc), intType)
-      | .FloorDiv _ => return (.intDiv lhs rhs (loc := loc), intType)
-      | .Mod _ => return (.intMod lhs rhs (loc := loc), intType)
+      | .FloorDiv _ =>
+        unless divisorPositive do
+          specWarning loc
+            "Python `//` (floor) and Laurel `Div` (Euclidean) only agree when the divisor is a positive literal; generated VC may diverge from runtime semantics for negative or symbolic divisors"
+        return (.intDiv lhs rhs (loc := loc), intType)
+      | .Mod _ =>
+        unless divisorPositive do
+          specWarning loc
+            "Python `%` (sign-of-divisor) and Laurel `Mod` (Euclidean) only agree when the divisor is a positive literal; generated VC may diverge from runtime semantics for negative or symbolic divisors"
+        return (.intMod lhs rhs (loc := loc), intType)
       | _ =>
         specWarning loc s!"unsupported BinOp in predicate: {repr op}"
         return placeholder
diff --git a/StrataTestExtra/Languages/Python/Specs/warnings.py b/StrataTestExtra/Languages/Python/Specs/warnings.py
index 3c0dac6863..c6c43693db 100644
--- a/StrataTestExtra/Languages/Python/Specs/warnings.py
+++ b/StrataTestExtra/Languages/Python/Specs/warnings.py
@@ -30,3 +30,11 @@ def for_else_loop(**kw: Unpack[LoopRequest]) -> None:
 # Skipped Expr in function body (non-ellipsis expression statement)
 def skipped_expr(**kw: int) -> None:
     kw["a"]
+
+# Floor division with a non-positive-literal divisor: Python `//` and
+# Laurel `Div` (Euclidean) only agree when the divisor is a positive
+# literal, so the recognizer emits a warning.
+DivArgs = TypedDict('DivArgs', {'x': int, 'y': int})
+
+def floor_div_symbolic_divisor(**kw: Unpack[DivArgs]) -> None:
+    assert kw["x"] // kw["y"] >= 0, "x // y >= 0"
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index 440172eb93..8a54b64b61 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -275,11 +275,12 @@ meta def warningTestCase : IO Unit := withPython fun pythonCmd => do
           throw <| IO.userError "Expected warnings from warnings.py but got none"
         -- Check for specific expected warning substrings
         let expectedWarnings := #[
-          "unsupported comparison",               -- assert kw["x"] == 1
+          "unsupported comparison",               -- chained comparison
           "unsupported __init__ assignment",   -- self.name = "hello"
           "skipped Assign in function body",   -- x = kw["a"]
           "For: else clause not supported",    -- for/else loop
-          "skipped Expr in function body"      -- kw["a"] (bare expression)
+          "skipped Expr in function body",     -- kw["a"] (bare expression)
+          "Python `//` (floor) and Laurel `Div`" -- non-positive divisor
         ]
         for expected in expectedWarnings do
           if !warnings.any (containsSubstr · expected) then

From 8f31fda103aff768c25c97c8a2329be7ad76040b Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 13:35:32 -0700
Subject: [PATCH 4/7] pyspec: warn when comparison defaults Any/Any operands to
 int

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.
---
 Strata/Languages/Python/Specs.lean            | 53 ++++++++++++-------
 .../Languages/Python/Specs/warnings.py        |  9 ++++
 .../Languages/Python/SpecsTest.lean           |  3 +-
 3 files changed, 44 insertions(+), 21 deletions(-)

diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index e655f1ae83..40b556835e 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -789,38 +789,51 @@ def assumeCondition (cond : SpecExpr) (loc : SourceRange) (act : SpecAssertionM
     { a with formula := .implies cond a.formula loc }
   modify fun s => { s with assertions := prevAssertions ++ wrapped }
 
-/-- Build a comparison expression dispatching to float or int variants based on type. -/
+/-- Build a comparison expression dispatching to float or int variants
+    based on type. Emits a `specWarning` when both operands are
+    `Any`-typed (e.g. unparameterised callees) and the recognizer has
+    to assume `int`: if the actual runtime values are floats the
+    generated SMT VC will have the wrong sort. -/
 private def makeComparison
+    (loc : SourceRange)
     (floatCtor intCtor : SpecExpr → SpecExpr → SpecExpr)
     (subj : SpecExpr) (subjType : SpecType) (bound : SpecExpr) (boundType : SpecType)
-    : Option SpecExpr :=
+    : SpecAssertionM (Option SpecExpr) :=
   if subjType.isFloatType then
     match bound with
-    | .floatLit .. => some (floatCtor subj bound)
-    | .intLit v loc => some (floatCtor subj (.floatLit (toString v) (loc := loc)))
-    | _ => none
+    | .floatLit .. => return some (floatCtor subj bound)
+    | .intLit v loc => return some (floatCtor subj (.floatLit (toString v) (loc := loc)))
+    | _ => return none
   else if subjType.isIntType then
     match bound with
-    | .intLit .. => some (intCtor subj bound)
+    | .intLit .. => return some (intCtor subj bound)
     | _ =>
       -- subj is int, bound is int- or Any-typed (a parameter etc.) →
       -- use the int comparison constructor.
-      if boundType.isIntType || boundType.isAnyType then some (intCtor subj bound) else none
+      if boundType.isIntType || boundType.isAnyType then
+        return some (intCtor subj bound)
+      else return none
   else if boundType.isFloatType then
     match bound with
-    | .floatLit .. => some (floatCtor subj bound)
-    | _ => none
+    | .floatLit .. => return some (floatCtor subj bound)
+    | _ => return none
   else if boundType.isIntType then
     match bound with
-    | .intLit .. => some (intCtor subj bound)
+    | .intLit .. => return some (intCtor subj bound)
     | _ =>
-      if subjType.isIntType || subjType.isAnyType then some (intCtor subj bound) else none
+      if subjType.isIntType || subjType.isAnyType then
+        return some (intCtor subj bound)
+      else return none
   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)
+    -- aren't seeded). Assume int — if the runtime values are floats,
+    -- the generated SMT VC will have the wrong sort, so warn.
+    do
+      specWarning loc
+        "comparison between Any-typed operands; assuming int — generated VC may be unsound if runtime values are floats"
+      return some (intCtor subj bound)
   else
-    none
+    return none
 
 private def transCompare (loc : SourceRange)
     (lhsExpr : SpecExpr) (lhsType : SpecType)
@@ -869,17 +882,17 @@ private def transCompare (loc : SourceRange)
 
   match ops[0] with
   | .GtE _ =>
-    return makeComparison (.floatGe · · (loc := loc)) (.intGe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatGe · · (loc := loc)) (.intGe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .LtE _ =>
-    return makeComparison (.floatLe · · (loc := loc)) (.intLe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatLe · · (loc := loc)) (.intLe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .Gt _ =>
-    return makeComparison (.floatGt · · (loc := loc)) (.intGt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatGt · · (loc := loc)) (.intGt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .Lt _ =>
-    return makeComparison (.floatLt · · (loc := loc)) (.intLt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatLt · · (loc := loc)) (.intLt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .Eq _ =>
-    return makeComparison (.floatEq · · (loc := loc)) (.intEq · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatEq · · (loc := loc)) (.intEq · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | .NotEq _ =>
-    return makeComparison (.floatNe · · (loc := loc)) (.intNe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+    makeComparison loc (.floatNe · · (loc := loc)) (.intNe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | _ =>
     return none
 
diff --git a/StrataTestExtra/Languages/Python/Specs/warnings.py b/StrataTestExtra/Languages/Python/Specs/warnings.py
index c6c43693db..1897cf3109 100644
--- a/StrataTestExtra/Languages/Python/Specs/warnings.py
+++ b/StrataTestExtra/Languages/Python/Specs/warnings.py
@@ -38,3 +38,12 @@ def skipped_expr(**kw: int) -> None:
 
 def floor_div_symbolic_divisor(**kw: Unpack[DivArgs]) -> None:
     assert kw["x"] // kw["y"] >= 0, "x // y >= 0"
+
+# Comparison between two `Any`-typed operands. The recognizer can't
+# tell whether the operands are int or float and assumes int; if the
+# runtime values are floats the generated VC has the wrong sort, so a
+# warning is emitted.
+AnyArgs = TypedDict('AnyArgs', {'x': Any, 'y': Any})
+
+def compare_any_to_any(**kw: Unpack[AnyArgs]) -> None:
+    assert kw["x"] < kw["y"], "x < y"
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index 8a54b64b61..ef71288a12 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -280,7 +280,8 @@ meta def warningTestCase : IO Unit := withPython fun pythonCmd => do
           "skipped Assign in function body",   -- x = kw["a"]
           "For: else clause not supported",    -- for/else loop
           "skipped Expr in function body",     -- kw["a"] (bare expression)
-          "Python `//` (floor) and Laurel `Div`" -- non-positive divisor
+          "Python `//` (floor) and Laurel `Div`", -- non-positive divisor
+          "comparison between Any-typed operands" -- both operands Any-typed
         ]
         for expected in expectedWarnings do
           if !warnings.any (containsSubstr · expected) then

From 6b11888904eb96b39a6e65cf128df854802f8ab6 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 13:39:58 -0700
Subject: [PATCH 5/7] pyspec: surface a clear warning for float arithmetic in
 predicates

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.
---
 Strata/Languages/Python/Specs.lean                 | 10 ++++++++++
 StrataTestExtra/Languages/Python/Specs/warnings.py |  9 +++++++++
 StrataTestExtra/Languages/Python/SpecsTest.lean    |  3 ++-
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 40b556835e..2910729c23 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -982,6 +982,16 @@ partial def transExpr (e : expr SourceRange)
       | _ =>
         specWarning loc s!"unsupported BinOp in predicate: {repr op}"
         return placeholder
+    else if lhsTp.isFloatType || rhsTp.isFloatType then
+      -- Float arithmetic in predicate bodies is deliberately deferred:
+      -- Laurel `Real` arithmetic models exact mathematical reals, but
+      -- Python floats are IEEE-754 doubles, so a faithful encoding
+      -- needs a `Float64` lowering path that doesn't yet exist in
+      -- `ToLaurel.lean`. Fall through with an explicit warning rather
+      -- than silently producing a `Real`-typed VC.
+      specWarning loc
+        s!"float arithmetic in predicates is not yet supported (op={repr op}); use the int variant or restructure the assertion"
+      return placeholder
     else
       specWarning loc s!"BinOp with non-int operand: lhs={repr lhsTp}, rhs={repr rhsTp}"
       return placeholder
diff --git a/StrataTestExtra/Languages/Python/Specs/warnings.py b/StrataTestExtra/Languages/Python/Specs/warnings.py
index 1897cf3109..99d17b147b 100644
--- a/StrataTestExtra/Languages/Python/Specs/warnings.py
+++ b/StrataTestExtra/Languages/Python/Specs/warnings.py
@@ -47,3 +47,12 @@ def floor_div_symbolic_divisor(**kw: Unpack[DivArgs]) -> None:
 
 def compare_any_to_any(**kw: Unpack[AnyArgs]) -> None:
     assert kw["x"] < kw["y"], "x < y"
+
+# Float arithmetic in predicate bodies is deliberately deferred — the
+# recognizer can't honestly emit Real-typed VCs for IEEE-754 floats —
+# so a warning is emitted instead of silently dropping into the int
+# branch.
+FloatArgs = TypedDict('FloatArgs', {'x': float, 'y': float})
+
+def float_arith_unsupported(**kw: Unpack[FloatArgs]) -> None:
+    assert kw["x"] + kw["y"] >= 0.0, "x + y >= 0"
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index ef71288a12..18a4f13b9a 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -281,7 +281,8 @@ meta def warningTestCase : IO Unit := withPython fun pythonCmd => do
           "For: else clause not supported",    -- for/else loop
           "skipped Expr in function body",     -- kw["a"] (bare expression)
           "Python `//` (floor) and Laurel `Div`", -- non-positive divisor
-          "comparison between Any-typed operands" -- both operands Any-typed
+          "comparison between Any-typed operands", -- both operands Any-typed
+          "float arithmetic in predicates is not yet supported" -- deferred float arith
         ]
         for expected in expectedWarnings do
           if !warnings.any (containsSubstr · expected) then

From 3e7ce904555e0f82e30b4a4a93420aa3abf073ae Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 13:45:24 -0700
Subject: [PATCH 6/7] pyspec: pin toDDM / fromDDM round-trip for new SpecExpr
 ctors
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 Strata/Languages/Python/Specs/DDM.lean        |  2 +-
 Strata/Languages/Python/Specs/Decls.lean      | 11 ++++++
 .../Languages/Python/SpecsTest.lean           | 38 +++++++++++++++++++
 3 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/Strata/Languages/Python/Specs/DDM.lean b/Strata/Languages/Python/Specs/DDM.lean
index 54b88e9cc9..697e00e122 100644
--- a/Strata/Languages/Python/Specs/DDM.lean
+++ b/Strata/Languages/Python/Specs/DDM.lean
@@ -444,7 +444,7 @@ private def DDM.ArgDecl.fromDDM (d : DDM.ArgDecl SourceRange) : Specs.Arg :=
     default := default.map (·.fromDDM)
   }
 
-private def DDM.SpecExprDecl.fromDDM (d : DDM.SpecExprDecl SourceRange) : Specs.SpecExpr :=
+protected def DDM.SpecExprDecl.fromDDM (d : DDM.SpecExprDecl SourceRange) : Specs.SpecExpr :=
   match d with
   | .placeholderExpr loc => .placeholder loc
   | .varExpr loc ⟨_, name⟩ => .var name loc
diff --git a/Strata/Languages/Python/Specs/Decls.lean b/Strata/Languages/Python/Specs/Decls.lean
index b73023bdb6..125006dbb0 100644
--- a/Strata/Languages/Python/Specs/Decls.lean
+++ b/Strata/Languages/Python/Specs/Decls.lean
@@ -488,6 +488,17 @@ inductive SpecExpr where
     Used in preconditions like `assert len(name) >= 1`. -/
 | stringLen (subject : SpecExpr) (loc : SourceRange)
 | intLit (value : Int) (loc : SourceRange)
+-- TODO(refactor): collapse the int{Ge,Le,Gt,Lt,Eq,Ne} and
+-- int{Add,Sub,Mul,Div,Mod} families into two parameterised
+-- constructors `intCompare (op : IntCmp) (lhs rhs) (loc)` and
+-- `intBinOp (op : IntBinOp) (lhs rhs) (loc)` (and the same for
+-- floats). Each new operator currently forces synchronized edits in
+-- ~8 places (`SpecExpr` ctor, `softBEq`, the DDM `op` decl, `toDDM`,
+-- `fromDDM`, `specExprToLaurel`, `PythonLaurelTypedExpr` def, the
+-- recognizer in `Specs.lean`); a parameterised shape would reduce
+-- that to one match per family and turn the round-trip property
+-- `(toDDM ∘ fromDDM) e == e` into a one-liner per family. Out of
+-- scope for the predicate-ops PR — track via follow-up.
 | intGe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
 | intLe (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
 | intGt (subject : SpecExpr) (bound : SpecExpr) (loc : SourceRange)
diff --git a/StrataTestExtra/Languages/Python/SpecsTest.lean b/StrataTestExtra/Languages/Python/SpecsTest.lean
index 18a4f13b9a..58ad248117 100644
--- a/StrataTestExtra/Languages/Python/SpecsTest.lean
+++ b/StrataTestExtra/Languages/Python/SpecsTest.lean
@@ -366,4 +366,42 @@ meta def testIntRoundTrip (v : Int) : Bool :=
 #guard testIntRoundTrip (42)
 #guard testIntRoundTrip (-100)
 
+/-- Catches regressions where a hand-written `toDDM`/`fromDDM` pair
+    swaps operands or routes through the wrong DDM constructor.
+    The 13 SpecExpr arithmetic/comparison ctors added by this PR each
+    require synchronized edits across both directions; this property
+    pins them as a unit until the parameterised `intBinOp`/`intCompare`
+    refactor (see TODO above the ctor list in `Decls.lean`) lands. -/
+meta def testSpecExprDDMRoundTrip (e : SpecExpr) : Bool :=
+  (DDM.SpecExprDecl.fromDDM e.toDDM).softBEq e
+
+private meta def loc : SourceRange := SourceRange.none
+private meta def x : SpecExpr := .var "x" loc
+private meta def y : SpecExpr := .var "y" loc
+private meta def k : SpecExpr := .intLit 1 loc
+
+-- Pin every new comparison constructor.
+#guard testSpecExprDDMRoundTrip (.intGe x k loc)
+#guard testSpecExprDDMRoundTrip (.intLe x k loc)
+#guard testSpecExprDDMRoundTrip (.intGt x k loc)
+#guard testSpecExprDDMRoundTrip (.intLt x k loc)
+#guard testSpecExprDDMRoundTrip (.intEq x k loc)
+#guard testSpecExprDDMRoundTrip (.intNe x k loc)
+-- Operand asymmetry (lhs ≠ rhs) catches a fromDDM that swaps l/r.
+#guard testSpecExprDDMRoundTrip (.intGt x y loc)
+#guard testSpecExprDDMRoundTrip (.intLt x y loc)
+#guard testSpecExprDDMRoundTrip (.intEq x y loc)
+#guard testSpecExprDDMRoundTrip (.intNe x y loc)
+-- Pin every new arithmetic constructor, with operand asymmetry.
+#guard testSpecExprDDMRoundTrip (.intAdd x y loc)
+#guard testSpecExprDDMRoundTrip (.intSub x y loc)
+#guard testSpecExprDDMRoundTrip (.intMul x y loc)
+#guard testSpecExprDDMRoundTrip (.intDiv x y loc)
+#guard testSpecExprDDMRoundTrip (.intMod x y loc)
+-- Float comparison ctors (operand asymmetry).
+#guard testSpecExprDDMRoundTrip (.floatGt x y loc)
+#guard testSpecExprDDMRoundTrip (.floatLt x y loc)
+#guard testSpecExprDDMRoundTrip (.floatEq x y loc)
+#guard testSpecExprDDMRoundTrip (.floatNe x y loc)
+
 end Strata.Python.Specs

From 5e79273fe86fb601ea569a86ab93228ee18c06ac Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 13:49:51 -0700
Subject: [PATCH 7/7] pyspec: pin Laurel VC body shape for new predicate
 operators
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 StrataTest/Languages/Python/ToLaurelTest.lean | 75 +++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/StrataTest/Languages/Python/ToLaurelTest.lean b/StrataTest/Languages/Python/ToLaurelTest.lean
index 534056eafa..8d7e09e948 100644
--- a/StrataTest/Languages/Python/ToLaurelTest.lean
+++ b/StrataTest/Languages/Python/ToLaurelTest.lean
@@ -836,4 +836,79 @@ private def translateFunc (args : Array Arg := #[])
   -- return type assume
   assert! body.contains "assume Any..isfrom_str(result)"
 
+/-! ## Predicate operator VC shape -/
+
+private def predFor (formula : SpecExpr) (args : Array Arg := #[arg "x" int, arg "y" int])
+    : String × Nat := translatePrecond
+  #[{ message := #[.str "p"], formula }] (args := args)
+
+-- intGt: x > 1
+#eval do
+  let (body, errs) := predFor (.intGt (.var "x" loc) (.intLit 1 loc) loc)
+  assert! errs == 0
+  assert! body.contains "Any..as_int!(x) > Any..as_int!"
+
+-- intLt: x < y (asymmetric: a swap would render the operands reversed)
+#eval do
+  let (body, errs) := predFor (.intLt (.var "x" loc) (.var "y" loc) loc)
+  assert! errs == 0
+  assert! body.contains "Any..as_int!(x) < Any..as_int!(y)"
+
+-- intEq: x == 0
+#eval do
+  let (body, errs) := predFor (.intEq (.var "x" loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "Any..as_int!(x) == Any..as_int!"
+
+-- intNe: x != y
+#eval do
+  let (body, errs) := predFor (.intNe (.var "x" loc) (.var "y" loc) loc)
+  assert! errs == 0
+  assert! body.contains "Any..as_int!(x) != Any..as_int!(y)"
+
+-- intAdd: x + y >= 0  (arithmetic wraps via from_int and feeds intGe)
+#eval do
+  let (body, errs) := predFor
+    (.intGe (.intAdd (.var "x" loc) (.var "y" loc) loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "from_int(Any..as_int!(x) + Any..as_int!(y))"
+
+-- intSub: x - y
+#eval do
+  let (body, errs) := predFor
+    (.intGe (.intSub (.var "x" loc) (.var "y" loc) loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "from_int(Any..as_int!(x) - Any..as_int!(y))"
+
+-- intMul: x * y
+#eval do
+  let (body, errs) := predFor
+    (.intGe (.intMul (.var "x" loc) (.var "y" loc) loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "from_int(Any..as_int!(x) * Any..as_int!(y))"
+
+-- intDiv: x // y  (Python `//` lowers to Laurel `Div` → ` / ` in output)
+#eval do
+  let (body, errs) := predFor
+    (.intGe (.intDiv (.var "x" loc) (.var "y" loc) loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "from_int(Any..as_int!(x) / Any..as_int!(y))"
+
+-- intMod: x % y
+#eval do
+  let (body, errs) := predFor
+    (.intGe (.intMod (.var "x" loc) (.var "y" loc) loc) (.intLit 0 loc) loc)
+  assert! errs == 0
+  assert! body.contains "from_int(Any..as_int!(x) % Any..as_int!(y))"
+
+-- floatLt sample: confirms float branch routes through `Any..as_float!`,
+-- not `Any..as_int!`; an int/float swap regression would fail this.
+#eval do
+  let (body, errs) := predFor
+    (.floatLt (.var "x" loc) (.var "y" loc) loc)
+    (args := #[arg "x" float_, arg "y" float_])
+  assert! errs == 0
+  assert! body.contains "Any..as_float!(x) < Any..as_float!(y)"
+  assert! !body.contains "Any..as_int!(x)"
+
 end Strata.Python.Specs.ToLaurel.Tests