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

[tautschnig]

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.

[Copilot]

Pull request overview

Adds a Laurel-to-Laurel transformation pass intended to prevent division-by-zero by inserting assert divisor != 0 before division/modulo operations, with a new CLI command to run the pass + verification and a new test suite for the transformation.

Changes:

• Introduce insertDivisionByZeroChecks Laurel transformation to add non-zero divisor assertions.
• Add unit + end-to-end tests for the transformation and verification behavior.
• Add laurelDivCheck CLI command and register it under the “Laurel” command group.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.

File	Description
Strata/Languages/Laurel/DivisionByZeroCheck.lean	Implements the div-by-zero assertion insertion pass.
StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean	Adds unit tests for AST output and an e2e verification test for unsafe division.
StrataMain.lean	Adds and wires a laurelDivCheck command to run the pass and verification.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[joscoh]

I haven't looked in detail yet, but is there a reason this does not just translate to the Core safe division/mod operators which automatically do this check?

[tautschnig]

I haven't looked in detail yet, but is there a reason this does not just translate to the Core safe division/mod operators which automatically do this check?

Thank you, I simply wasn't aware of their existence! Implementation completely reworked in the latest commit, pull-request description updated to reflect what actually happens.

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated 2 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[keyboardDrummer]

Some thoughts on how this connects to source languages.

In Java, dividing an integer by zero throws an ArithmeticException, so there are valid Java programs that divide integers by zero. However, I think this just means we need to wrap Laurel division when encoding Java division in Laurel. It still seems good if Laurel integer division does not allow dividing by zero.

Example (uses some made-up-syntax for exception handling):

// Laurel
function JavaDivision(top: int, bottom: int): int
  throws ArithmeticException on bottom == 0 
{
  if (bottom == 0)
    throw new ArithmeticException();
  else 
    top / bottom
}

[keyboardDrummer]

Sweet! Thanks

[tautschnig]

In Java, dividing an integer by zero throws an ArithmeticException, so there are valid Java programs that divide integers by zero. However, I think this just means we need to wrap Laurel division when encoding Java division in Laurel.

Yes, I think it would just mean the preconditions of SafeDiv are guaranteed to be upheld.

BTW: the tooling that compiles Java to Laurel may have to enable the passes that create those ArithmeticException runtime checks: there's a variant of the above where a valid Java program even catches that exception and does something non-trivial in that case.

[joehendrix]

Reapproved after reviewing the latest change — function-call syntax for unchecked divt/modt CST nodes looks good.