Skip to content

Commit 9cf52ec

Browse files
tautschnigkiro-agent
authored and
kondylidou
committed
Add division-by-zero verification for Laurel via Core safe operators (strata-org#510)
Laurel division and modulo operations (/, %, /t, %t) now fail verification when the divisor may be zero. This is achieved by translating Laurel's division/modulo to Core's safe operator variants (Int.SafeDiv, Int.SafeMod, Int.SafeDivT, Int.SafeModT), which carry a built-in y ≠ 0 precondition. The existing PrecondElim transform then automatically generates the necessary verification conditions at each use site — no Laurel-level instrumentation is required. *Description of changes:* New Core operators — Int.SafeDivT and Int.SafeModT added to the Lambda IntBoolFactory and Core Factory, mirroring the existing Int.SafeDiv/Int.SafeMod. SMT encoding and AST-to-CST printing updated accordingly. Laurel-to-Core translator — Div/Mod/DivT/ModT now emit the safe operator variants instead of the unchecked ones. End-to-end tests — New DivisionByZeroCheckTest.lean verifies: - Safe division with a known non-zero divisor passes ✅ - Division by an unconstrained parameter fails ❌ - A pure function with an explicit requires y != 0 precondition passes, but callers that don't satisfy it fail ❌ Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent 0cddd8f commit 9cf52ec

File tree

13 files changed

+120
-24
lines changed

13 files changed

+120
-24
lines changed

‎Strata/DL/Lambda/IntBoolFactory.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -293,6 +293,14 @@ def intSafeModFunc : WFLFunc T :=
293293
binaryOp (InValTy := Int) "Int.SafeMod" (· % ·) (· != 0)
294294
(preconditions := [yNeZeroPrecond])
295295

296+
def intSafeDivTFunc : WFLFunc T :=
297+
binaryOp (InValTy := Int) "Int.SafeDivT" Int.tdiv (· != 0)
298+
(preconditions := [yNeZeroPrecond])
299+
300+
def intSafeModTFunc : WFLFunc T :=
301+
binaryOp (InValTy := Int) "Int.SafeModT" Int.tmod (· != 0)
302+
(preconditions := [yNeZeroPrecond])
303+
296304
end
297305

298306
def IntBoolFactory [Inhabited T.mono.base.Metadata] : @Factory T := (#[
@@ -304,7 +312,9 @@ def IntBoolFactory [Inhabited T.mono.base.Metadata] : @Factory T := (#[
304312
intModFunc,
305313
intSafeModFunc,
306314
intDivTFunc,
315+
intSafeDivTFunc,
307316
intModTFunc,
317+
intSafeModTFunc,
308318
intNegFunc,
309319
intLtFunc,
310320
intLeFunc,

‎Strata/Languages/Core/DDMTransform/ASTtoCST.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -528,6 +528,10 @@ def handleBinaryOps {M} [Inhabited M] (name : String)
528528
| "Int.SafeDiv" => pure (.safediv_expr default ty arg1 arg2)
529529
| "Int.Mod" => pure (.mod_expr default ty arg1 arg2)
530530
| "Int.SafeMod" => pure (.safemod_expr default ty arg1 arg2)
531+
| "Int.DivT" => pure (.divt_expr default ty arg1 arg2)
532+
| "Int.SafeDivT" => pure (.safedivt_expr default ty arg1 arg2)
533+
| "Int.ModT" => pure (.modt_expr default ty arg1 arg2)
534+
| "Int.SafeModT" => pure (.safemodt_expr default ty arg1 arg2)
531535
| "Int.Le" | "Real.Le" => pure (.le default ty arg1 arg2)
532536
| "Int.Lt" | "Real.Lt" => pure (.lt default ty arg1 arg2)
533537
| "Int.Ge" | "Real.Ge" => pure (.ge default ty arg1 arg2)

‎Strata/Languages/Core/DDMTransform/Grammar.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,10 @@ fn div_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " div "
131131
fn mod_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " mod " b;
132132
fn safediv_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " / " b;
133133
fn safemod_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " % " b;
134+
fn divt_expr (tp : Type, a : tp, b : tp) : tp => "Int.DivT(" a ", " b ")";
135+
fn modt_expr (tp : Type, a : tp, b : tp) : tp => "Int.ModT(" a ", " b ")";
136+
fn safedivt_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " /t " b;
137+
fn safemodt_expr (tp : Type, a : tp, b : tp) : tp => @[prec(30), leftassoc] a " %t " b;
134138

135139
fn bvnot (tp : Type, a : tp) : tp => "~" a;
136140
fn bvand (tp : Type, a : tp, b : tp) : tp => @[prec(20), leftassoc] a " & " b;

‎Strata/Languages/Core/DDMTransform/Translate.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -507,6 +507,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres
507507
| .some .int, q`Core.mod_expr => return Core.intModOp
508508
| .some .int, q`Core.safediv_expr => return Core.intSafeDivOp
509509
| .some .int, q`Core.safemod_expr => return Core.intSafeModOp
510+
| .some .int, q`Core.divt_expr => return Core.intDivTOp
511+
| .some .int, q`Core.modt_expr => return Core.intModTOp
512+
| .some .int, q`Core.safedivt_expr => return Core.intSafeDivTOp
513+
| .some .int, q`Core.safemodt_expr => return Core.intSafeModTOp
510514
| .some .int, q`Core.neg_expr => return Core.intNegOp
511515

512516
| .some .real, q`Core.le => return Core.realLeOp
@@ -888,6 +892,10 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
888892
| q`Core.safediv_expr
889893
| q`Core.mod_expr
890894
| q`Core.safemod_expr
895+
| q`Core.divt_expr
896+
| q`Core.modt_expr
897+
| q`Core.safedivt_expr
898+
| q`Core.safemodt_expr
891899
| q`Core.bvand
892900
| q`Core.bvor
893901
| q`Core.bvxor

‎Strata/Languages/Core/Factory.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,7 +314,9 @@ def WFFactory : Lambda.WFLFactory CoreLParams :=
314314
intModFunc (T := CoreLParams),
315315
intSafeModFunc (T := CoreLParams),
316316
intDivTFunc (T := CoreLParams),
317+
intSafeDivTFunc (T := CoreLParams),
317318
intModTFunc (T := CoreLParams),
319+
intSafeModTFunc (T := CoreLParams),
318320
intNegFunc (T := CoreLParams),
319321

320322
intLtFunc (T := CoreLParams),
@@ -426,7 +428,9 @@ def intSafeDivOp : Expression.Expr := (@intSafeDivFunc CoreLParams _ _).opExpr
426428
def intModOp : Expression.Expr := (@intModFunc CoreLParams _).opExpr
427429
def intSafeModOp : Expression.Expr := (@intSafeModFunc CoreLParams _ _).opExpr
428430
def intDivTOp : Expression.Expr := (@intDivTFunc CoreLParams _).opExpr
431+
def intSafeDivTOp : Expression.Expr := (@intSafeDivTFunc CoreLParams _ _).opExpr
429432
def intModTOp : Expression.Expr := (@intModTFunc CoreLParams _).opExpr
433+
def intSafeModTOp : Expression.Expr := (@intSafeModTFunc CoreLParams _ _).opExpr
430434
def intNegOp : Expression.Expr := (@intNegFunc CoreLParams _).opExpr
431435
def intLtOp : Expression.Expr := (@intLtFunc CoreLParams _).opExpr
432436
def intLeOp : Expression.Expr := (@intLeFunc CoreLParams _).opExpr

‎Strata/Languages/Core/SMTEncoder.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -382,7 +382,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
382382
| "Int.Mod" => .ok (.app Op.mod, .int , ctx)
383383
| "Int.SafeMod" => .ok (.app Op.mod, .int , ctx)
384384
-- Truncating division: tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
385-
| "Int.DivT" =>
385+
| "Int.DivT" | "Int.SafeDivT" =>
386386
let divTApp := fun (args : List Term) (retTy : TermType) =>
387387
match args with
388388
| [a, b] =>
@@ -398,7 +398,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
398398
.ok (divTApp, .int, ctx)
399399
-- Truncating modulo: tmod(a,b) = a - b * tdiv(a,b)
400400
-- tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
401-
| "Int.ModT" =>
401+
| "Int.ModT" | "Int.SafeModT" =>
402402
let modTApp := fun (args : List Term) (retTy : TermType) =>
403403
match args with
404404
| [a, b] =>

‎Strata/Languages/Laurel/LaurelToCoreTranslator.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ import Strata.Languages.Laurel.LaurelFormat
2323
import Strata.Util.Tactics
2424

2525
open Core (VCResult VCResults VerifyOptions)
26-
open Core (intAddOp intSubOp intMulOp intDivOp intModOp intDivTOp intModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
26+
open Core (intAddOp intSubOp intMulOp intSafeDivOp intSafeModOp intSafeDivTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
2727

2828
namespace Strata.Laurel
2929

@@ -161,10 +161,10 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd)
161161
| .Add => return binOp intAddOp
162162
| .Sub => return binOp intSubOp
163163
| .Mul => return binOp intMulOp
164-
| .Div => return binOp intDivOp
165-
| .Mod => return binOp intModOp
166-
| .DivT => return binOp intDivTOp
167-
| .ModT => return binOp intModTOp
164+
| .Div => return binOp intSafeDivOp
165+
| .Mod => return binOp intSafeModOp
166+
| .DivT => return binOp intSafeDivTOp
167+
| .ModT => return binOp intSafeModTOp
168168
| .Lt => return binOp intLtOp
169169
| .Leq => return binOp intLeOp
170170
| .Gt => return binOp intGtOp

‎Strata/Languages/Python/PythonToLaurel.lean‎

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -476,13 +476,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
476476
let target := name.val
477477
let valueExpr ← translateExpr ctx value
478478
let targetExpr := mkStmtExprMd (StmtExpr.Identifier target)
479-
let assignStmt := mkStmtExprMd (StmtExpr.Assign [targetExpr] valueExpr)
479+
let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] valueExpr) md
480480
return (ctx, assignStmt)
481481
| .Attribute _ obj attr _ =>
482482
-- Field assignment: obj.field = expr or self.field = expr
483483
let valueExpr ← translateExpr ctx value
484484
let targetExpr ← translateExpr ctx targets.val[0]! -- This will handle self.field via translateExpr
485-
let assignStmt := mkStmtExprMd (StmtExpr.Assign [targetExpr] valueExpr)
485+
let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] valueExpr) md
486486
return (ctx, assignStmt)
487487
| _ => throw (.unsupportedConstruct "Only simple variable or field assignment supported" (toString (repr s)))
488488

@@ -501,7 +501,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
501501
let fieldAccess := mkStmtExprMd (StmtExpr.FieldSelect
502502
(mkStmtExprMd (StmtExpr.Identifier "self"))
503503
attr.val)
504-
let assignStmt := mkStmtExprMd (StmtExpr.Assign [fieldAccess] valueExpr)
504+
let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [fieldAccess] valueExpr) md
505505
return (ctx, assignStmt)
506506
else
507507
throw (.unsupportedConstruct "Only self.field assignments supported in methods" (toString (repr s)))
@@ -535,7 +535,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
535535
let translatedArgs ← args.val.toList.mapM (translateExpr ctx)
536536

537537
let newExpr := mkStmtExprMd (StmtExpr.New funcName)
538-
let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType (some newExpr))
538+
let declStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable varName varType (some newExpr)) md
539539

540540
let initCall := mkStmtExprMd (StmtExpr.InstanceCall
541541
(mkStmtExprMd (StmtExpr.Identifier varName))
@@ -547,16 +547,18 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
547547
else
548548
-- Regular call, not a constructor
549549
let initVal ← translateCall ctx f args.val.toList
550-
let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType (some initVal))
550+
let initVal := { initVal with md := md }
551+
let declStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable varName varType (some initVal)) md
551552
return (newCtx, declStmt)
552553
| some initExpr => do
553554
-- Regular annotated assignment with initializer
554555
let initVal ← translateExpr newCtx initExpr
555-
let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType (some initVal))
556+
let initVal := { initVal with md := md }
557+
let declStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable varName varType (some initVal)) md
556558
return (newCtx, declStmt)
557559
| none =>
558560
-- Declaration without initializer
559-
let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType none)
561+
let declStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable varName varType none) md
560562
return (newCtx, declStmt)
561563

562564
-- If statement
@@ -583,13 +585,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
583585
else do
584586
let (_, elseStmts) ← translateStmtList bodyCtx orelse.val.toList
585587
.ok (some (mkStmtExprMd (StmtExpr.Block elseStmts none)))
586-
let ifStmt := mkStmtExprMd (StmtExpr.IfThenElse finalCondExpr bodyBlock elseBlock)
588+
let ifStmt := mkStmtExprMdWithLoc (StmtExpr.IfThenElse finalCondExpr bodyBlock elseBlock) md
587589

588590
-- Wrap in block if we hoisted condition
589591
let result := if condStmts.isEmpty then
590592
ifStmt
591593
else
592-
mkStmtExprMd (StmtExpr.Block (condStmts ++ [ifStmt]) none)
594+
mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [ifStmt]) none) md
593595

594596
return (bodyCtx, result)
595597

@@ -610,13 +612,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
610612

611613
let (loopCtx, bodyStmts) ← translateStmtList condCtx body.val.toList
612614
let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none)
613-
let whileStmt := mkStmtExprMd (StmtExpr.While finalCondExpr [] none bodyBlock)
615+
let whileStmt := mkStmtExprMdWithLoc (StmtExpr.While finalCondExpr [] none bodyBlock) md
614616

615617
-- Wrap in block if we hoisted condition
616618
let result := if condStmts.isEmpty then
617619
whileStmt
618620
else
619-
mkStmtExprMd (StmtExpr.Block (condStmts ++ [whileStmt]) none)
621+
mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [whileStmt]) none) md
620622

621623
return (loopCtx, result)
622624

@@ -627,7 +629,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
627629
let e ← translateExpr ctx expr
628630
.ok (some e)
629631
| none => .ok none
630-
let retStmt := mkStmtExprMd (StmtExpr.Return retVal)
632+
let retStmt := mkStmtExprMdWithLoc (StmtExpr.Return retVal) md
631633
return (ctx, retStmt)
632634

633635
-- Assert statement
@@ -650,13 +652,14 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
650652
let result := if condStmts.isEmpty then
651653
assertStmt
652654
else
653-
mkStmtExprMd (StmtExpr.Block (condStmts ++ [assertStmt]) none)
655+
mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [assertStmt]) none) md
654656

655657
return (condCtx, result)
656658

657659
-- Expression statement (e.g., function call)
658660
| .Expr _ value => do
659661
let expr ← translateExpr ctx value
662+
let expr := { expr with md := md }
660663
return (ctx, expr)
661664

662665
| .Import _ _ | .ImportFrom _ _ _ _ => return (ctx, mkStmtExprMd .Hole)
@@ -690,7 +693,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
690693
let handlerBlock := mkStmtExprMd (StmtExpr.Block handlerStmts (some handlerLabel))
691694

692695
-- Wrap in try block
693-
let tryBlock := mkStmtExprMd (StmtExpr.Block (bodyStmtsWithChecks ++ [handlerBlock]) (some tryLabel))
696+
let tryBlock := mkStmtExprMdWithLoc (StmtExpr.Block (bodyStmtsWithChecks ++ [handlerBlock]) (some tryLabel)) md
694697
return (bodyCtx, tryBlock)
695698

696699
| .Raise _ _ _ => return (ctx, mkStmtExprMd .Hole)
@@ -717,7 +720,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
717720
-- Create: { target = havoc; body_statements }
718721
-- This abstracts: execute body once with arbitrary target value
719722
let targetDecl := mkStmtExprMd (StmtExpr.LocalVariable targetName targetType (some (mkStmtExprMd .Hole)))
720-
let loopBlock := mkStmtExprMd (StmtExpr.Block ([targetDecl] ++ bodyStmts) none)
723+
let loopBlock := mkStmtExprMdWithLoc (StmtExpr.Block ([targetDecl] ++ bodyStmts) none) md
721724

722725
return (finalCtx, loopBlock)
723726

‎StrataTest/DL/Lambda/TestGenTests.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ Lambda.LTy.forAll [] (Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.tcons "bool"
148148
in context
149149
{ types := [[]], aliases := [] }
150150
in factory
151-
#[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]
151+
#[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]
152152
-/
153153
#guard_msgs in
154154
#eval Strata.Util.withStdGenSeed 0 do
@@ -167,7 +167,7 @@ Lambda.LTy.forAll [] (Lambda.LMonoTy.tcons "arrow" [Lambda.LMonoTy.tcons "bool"
167167
in context
168168
{ types := [[]], aliases := [] }
169169
in factory
170-
#[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]
170+
#[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]
171171
-/
172172
#guard_msgs(info, drop error) in
173173
#eval Strata.Util.withStdGenSeed 0 do

‎StrataTest/Languages/Core/ProcedureEvalTests.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,11 @@ func Int.Mod : ((x : int) (y : int)) → int;
3838
func Int.SafeMod : ((x : int) (y : int)) → int
3939
requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
4040
func Int.DivT : ((x : int) (y : int)) → int;
41+
func Int.SafeDivT : ((x : int) (y : int)) → int
42+
requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
4143
func Int.ModT : ((x : int) (y : int)) → int;
44+
func Int.SafeModT : ((x : int) (y : int)) → int
45+
requires ((~Bool.Not : (arrow bool bool)) ((y : int) == #0));
4246
func Int.Neg : ((x : int)) → int;
4347
func Int.Lt : ((x : int) (y : int)) → bool;
4448
func Int.Le : ((x : int) (y : int)) → bool;

0 commit comments

Comments
 (0)