pyspec: extend predicate bodies with strict comparisons, equality, and integer arithmetic

Strata/Languages/Python/PythonLaurelTypedExpr.lean

@@ -74,6 +74,54 @@ 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 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
+
+/-- 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
+
+/-- 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
+
+
 def realGeq (x y : TypedStmtExpr .TReal)
     (source : Option FileRange := x.stmt.source) : TypedStmtExpr .TBool :=
   .ofStmt (.PrimitiveOp .Geq [x.stmt, y.stmt]) source
@@ -82,6 +130,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

Strata/Languages/Python/Specs.lean

@@ -789,30 +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)
-    | _ => none
+    | .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
+        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)
-    | _ => none
+    | .intLit .. => return some (intCtor subj bound)
+    | _ =>
+      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). 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)
@@ -825,7 +846,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 +855,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,16 +875,24 @@ 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
 
   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 _ =>
+    makeComparison loc (.floatGt · · (loc := loc)) (.intGt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .Lt _ =>
+    makeComparison loc (.floatLt · · (loc := loc)) (.intLt · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .Eq _ =>
+    makeComparison loc (.floatEq · · (loc := loc)) (.intEq · · (loc := loc)) lhsExpr lhsType boundExpr boundType
+  | .NotEq _ =>
+    makeComparison loc (.floatNe · · (loc := loc)) (.intNe · · (loc := loc)) lhsExpr lhsType boundExpr boundType
   | _ =>
     return none
 
@@ -916,6 +947,54 @@ 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
+    -- 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 _ =>
+        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
+    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
   -- String literal (extract value for use in messages)
   | .Constant _ (.ConString _ ⟨_, _s⟩) _ =>
     return (.placeholder (loc := loc), SpecType.ident loc .builtinsStr)

Strata/Languages/Python/Specs/DDM.lean

@@ -87,11 +87,37 @@ 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 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;
 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 +301,22 @@ 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
+  | .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
+  | .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, ·⟩)⟩
@@ -405,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
@@ -416,9 +455,22 @@ 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
+  | .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
+  | .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