Add division-by-zero verification for Laurel via Core safe operators

Strata/DL/Lambda/IntBoolFactory.lean

@@ -293,6 +293,14 @@ def intSafeModFunc : WFLFunc T :=
   binaryOp (InValTy := Int) "Int.SafeMod" (· % ·) (· != 0)
     (preconditions := [yNeZeroPrecond])
 
+def intSafeDivTFunc : WFLFunc T :=
+  binaryOp (InValTy := Int) "Int.SafeDivT" Int.tdiv (· != 0)
+    (preconditions := [yNeZeroPrecond])
+
+def intSafeModTFunc : WFLFunc T :=
+  binaryOp (InValTy := Int) "Int.SafeModT" Int.tmod (· != 0)
+    (preconditions := [yNeZeroPrecond])
+
 end
 
 def IntBoolFactory [Inhabited T.mono.base.Metadata] : @Factory T := (#[
@@ -304,7 +312,9 @@ def IntBoolFactory [Inhabited T.mono.base.Metadata] : @Factory T := (#[
     intModFunc,
     intSafeModFunc,
     intDivTFunc,
+    intSafeDivTFunc,
     intModTFunc,
+    intSafeModTFunc,
     intNegFunc,
     intLtFunc,
     intLeFunc,

Strata/Languages/Core/DDMTransform/ASTtoCST.lean

@@ -528,6 +528,10 @@ def handleBinaryOps {M} [Inhabited M] (name : String)
   | "Int.SafeDiv" => pure (.safediv_expr default ty arg1 arg2)
   | "Int.Mod" => pure (.mod_expr default ty arg1 arg2)
   | "Int.SafeMod" => pure (.safemod_expr default ty arg1 arg2)
+  | "Int.DivT" => pure (.safedivt_expr default ty arg1 arg2)
+  | "Int.SafeDivT" => pure (.safedivt_expr default ty arg1 arg2)
+  | "Int.ModT" => pure (.safemodt_expr default ty arg1 arg2)
+  | "Int.SafeModT" => pure (.safemodt_expr default ty arg1 arg2)
   | "Int.Le" | "Real.Le" => pure (.le default ty arg1 arg2)
   | "Int.Lt" | "Real.Lt" => pure (.lt default ty arg1 arg2)
   | "Int.Ge" | "Real.Ge" => pure (.ge default ty arg1 arg2)

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -131,6 +131,8 @@ fn div_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " div "
 fn mod_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " mod " b;
 fn safediv_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " / " b;
 fn safemod_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " % " b;
+fn safedivt_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " /t " b;
+fn safemodt_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " %t " b;
 
 fn bvnot (tp : Type, a : tp) : tp => "~" a;
 fn bvand (tp : Type, a : tp, b : tp) : tp => @[prec(20), leftassoc] a " & " b;

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -507,6 +507,8 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres
   | .some .int, q`Core.mod_expr => return Core.intModOp
   | .some .int, q`Core.safediv_expr => return Core.intSafeDivOp
   | .some .int, q`Core.safemod_expr => return Core.intSafeModOp
+  | .some .int, q`Core.safedivt_expr => return Core.intSafeDivTOp
+  | .some .int, q`Core.safemodt_expr => return Core.intSafeModTOp
   | .some .int, q`Core.neg_expr => return Core.intNegOp
 
   | .some .real, q`Core.le       => return Core.realLeOp
@@ -888,6 +890,8 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
     | q`Core.safediv_expr
     | q`Core.mod_expr
     | q`Core.safemod_expr
+    | q`Core.safedivt_expr
+    | q`Core.safemodt_expr
     | q`Core.bvand
     | q`Core.bvor
     | q`Core.bvxor

Strata/Languages/Core/Factory.lean

@@ -314,7 +314,9 @@ def WFFactory : Lambda.WFLFactory CoreLParams :=
   intModFunc (T := CoreLParams),
   intSafeModFunc (T := CoreLParams),
   intDivTFunc (T := CoreLParams),
+  intSafeDivTFunc (T := CoreLParams),
   intModTFunc (T := CoreLParams),
+  intSafeModTFunc (T := CoreLParams),
   intNegFunc (T := CoreLParams),
 
   intLtFunc (T := CoreLParams),
@@ -426,7 +428,9 @@ def intSafeDivOp : Expression.Expr := (@intSafeDivFunc CoreLParams _ _).opExpr
 def intModOp : Expression.Expr := (@intModFunc CoreLParams _).opExpr
 def intSafeModOp : Expression.Expr := (@intSafeModFunc CoreLParams _ _).opExpr
 def intDivTOp : Expression.Expr := (@intDivTFunc CoreLParams _).opExpr
+def intSafeDivTOp : Expression.Expr := (@intSafeDivTFunc CoreLParams _ _).opExpr
 def intModTOp : Expression.Expr := (@intModTFunc CoreLParams _).opExpr
+def intSafeModTOp : Expression.Expr := (@intSafeModTFunc CoreLParams _ _).opExpr
 def intNegOp : Expression.Expr := (@intNegFunc CoreLParams _).opExpr
 def intLtOp : Expression.Expr := (@intLtFunc CoreLParams _).opExpr
 def intLeOp : Expression.Expr := (@intLeFunc CoreLParams _).opExpr

Strata/Languages/Core/SMTEncoder.lean

@@ -382,7 +382,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
     | "Int.Mod"      => .ok (.app Op.mod,        .int ,   ctx)
     | "Int.SafeMod"  => .ok (.app Op.mod,        .int ,   ctx)
     -- Truncating division: tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
-    | "Int.DivT"     =>
+    | "Int.DivT" | "Int.SafeDivT" =>
       let divTApp := fun (args : List Term) (retTy : TermType) =>
         match args with
         | [a, b] =>
@@ -398,7 +398,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
       .ok (divTApp, .int, ctx)
     -- Truncating modulo: tmod(a,b) = a - b * tdiv(a,b)
     -- tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
-    | "Int.ModT"     =>
+    | "Int.ModT" | "Int.SafeModT" =>
       let modTApp := fun (args : List Term) (retTy : TermType) =>
         match args with
         | [a, b] =>

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -23,7 +23,7 @@ import Strata.Languages.Laurel.LaurelFormat
 import Strata.Util.Tactics
 
 open Core (VCResult VCResults VerifyOptions)
-open Core (intAddOp intSubOp intMulOp intDivOp intModOp intDivTOp intModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
+open Core (intAddOp intSubOp intMulOp intSafeDivOp intSafeModOp intSafeDivTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
 
 namespace Strata.Laurel
 
@@ -161,10 +161,10 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd)
     | .Add => return binOp intAddOp
     | .Sub => return binOp intSubOp
     | .Mul => return binOp intMulOp
-    | .Div => return binOp intDivOp
-    | .Mod => return binOp intModOp
-    | .DivT => return binOp intDivTOp
-    | .ModT => return binOp intModTOp
+    | .Div => return binOp intSafeDivOp
+    | .Mod => return binOp intSafeModOp
+    | .DivT => return binOp intSafeDivTOp
+    | .ModT => return binOp intSafeModTOp
     | .Lt => return binOp intLtOp
     | .Leq => return binOp intLeOp
     | .Gt => return binOp intGtOp

StrataTest/DL/Lambda/TestGenTests.lean

@@ -148,7 +148,7 @@ Lambda.LTy.forAll [] (Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.tcons "bool"
 in context
 { types := [[]], aliases := [] }
 in factory
-#[Int.Add, Int.Sub, Int.Mul, Int.Div, Int.SafeDiv, Int.Mod, Int.SafeMod, Int.DivT, Int.ModT, Int.Neg, Int.Lt, Int.Le, Int.Gt, Int.Ge, Bool.And, Bool.Or, Bool.Implies, Bool.Equiv, Bool.Not]
+#[Int.Add, Int.Sub, Int.Mul, Int.Div, Int.SafeDiv, Int.Mod, Int.SafeMod, Int.DivT, Int.SafeDivT, Int.ModT, Int.SafeModT, Int.Neg, Int.Lt, Int.Le, Int.Gt, Int.Ge, Bool.And, Bool.Or, Bool.Implies, Bool.Equiv, Bool.Not]
 -/
 #guard_msgs in
 #eval Strata.Util.withStdGenSeed 0 do
@@ -167,7 +167,7 @@ Lambda.LTy.forAll [] (Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.tcons "bool"
 in context
 { types := [[]], aliases := [] }
 in factory
-#[Int.Add, Int.Sub, Int.Mul, Int.Div, Int.SafeDiv, Int.Mod, Int.SafeMod, Int.DivT, Int.ModT, Int.Neg, Int.Lt, Int.Le, Int.Gt, Int.Ge, Bool.And, Bool.Or, Bool.Implies, Bool.Equiv, Bool.Not]
+#[Int.Add, Int.Sub, Int.Mul, Int.Div, Int.SafeDiv, Int.Mod, Int.SafeMod, Int.DivT, Int.SafeDivT, Int.ModT, Int.SafeModT, Int.Neg, Int.Lt, Int.Le, Int.Gt, Int.Ge, Bool.And, Bool.Or, Bool.Implies, Bool.Equiv, Bool.Not]
 -/
 #guard_msgs(info, drop error) in
 #eval Strata.Util.withStdGenSeed 0 do

StrataTest/Languages/Core/ProcedureEvalTests.lean

@@ -38,7 +38,11 @@ func Int.Mod :  ((x : int) (y : int)) → int;
 func Int.SafeMod :  ((x : int) (y : int)) → int
   requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
 func Int.DivT :  ((x : int) (y : int)) → int;
+func Int.SafeDivT :  ((x : int) (y : int)) → int
+  requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
 func Int.ModT :  ((x : int) (y : int)) → int;
+func Int.SafeModT :  ((x : int) (y : int)) → int
+  requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
 func Int.Neg :  ((x : int)) → int;
 func Int.Lt :  ((x : int) (y : int)) → bool;
 func Int.Le :  ((x : int) (y : int)) → bool;

StrataTest/Languages/Core/ProgramTypeTests.lean

@@ -111,7 +111,11 @@ info: ok: [(type Foo (a0 : Type, a1 : Type);
   func Int.SafeMod :  ((x : int) (y : int)) → int
     requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
   func Int.DivT :  ((x : int) (y : int)) → int;
+  func Int.SafeDivT :  ((x : int) (y : int)) → int
+    requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
   func Int.ModT :  ((x : int) (y : int)) → int;
+  func Int.SafeModT :  ((x : int) (y : int)) → int
+    requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
   func Int.Neg :  ((x : int)) → int;
   func Int.Lt :  ((x : int) (y : int)) → bool;
   func Int.Le :  ((x : int) (y : int)) → bool;

StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean

@@ -0,0 +1,54 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata.Laurel
+
+/-! ## End-to-end test: safe division (no errors) and unsafe division (error)
+
+Division and modulo in Laurel translate to Core's safe operators, which have
+built-in preconditions (divisor ≠ 0). The PrecondElim transform automatically
+generates verification conditions for these preconditions.
+-/
+
+def e2eProgram := r"
+procedure safeDivision() {
+  var x: int := 10;
+  var y: int := 2;
+  var z: int := x / y;
+  assert z == 5;
+}
+
+procedure unsafeDivision(x: int) {
+  var z: int := 10 / x;
+//              ^^^^^^ error: assertion does not hold
+}
+
+function pureDiv(x: int, y: int): int
+  requires y != 0
+{
+  x / y
+}
+
+procedure callPureDivSafe() {
+  var z: int := pureDiv(10, 2);
+  assert z == 5;
+}
+
+procedure callPureDivUnsafe(x: int) {
+  var z: int := pureDiv(10, x);
+//              ^^^^^^^^^^^^^^ error: assertion does not hold
+}
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "DivByZeroE2E" e2eProgram 22 processLaurelFile
+
+end Laurel

StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected

@@ -11,4 +11,5 @@ assert(102): ✅ pass (at line 7, col 4)
 assert(226): ✅ pass (at line 12, col 4)
 assert(345): ✅ pass (at line 16, col 4)
 assert(458): ✅ pass (at line 20, col 4)
+init_calls_Int.SafeDiv_0: ✅ pass
 assert(567): ✅ pass (at line 24, col 4)