Clarify the semantics of DIV_INT64 in LF spec. (#10003)

* Clarify semantics of DIV_INT64 in LF spec. Especially around negative operands. Adds a couple of unit tests to make sure the behavior stays this way, and that MOD_INT64 is consistent with DIV_INT64. changelog_begin changelog_end * spelling * scalafmt * hardcode numbers in MOD_INT64 test
digital-asset · Jun 15, 2021 · 0c32cf2 · 0c32cf2
1 parent b79e739
commit 0c32cf2
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 1 deletion.
diff --git a/daml-lf/interpreter/src/test/scala/com/digitalasset/daml/lf/speedy/SBuiltinTest.scala b/daml-lf/interpreter/src/test/scala/com/digitalasset/daml/lf/speedy/SBuiltinTest.scala
@@ -80,6 +80,13 @@ class SBuiltinTest extends AnyFreeSpec with Matchers with TableDrivenPropertyChe
     }
 
     "DIV_INT64" - {
+      "is symmetric, i.e. rounds towards 0" in {
+        eval(e"DIV_INT64 10 3") shouldBe Right(SInt64(3))
+        eval(e"DIV_INT64 10 -3") shouldBe Right(SInt64(-3))
+        eval(e"DIV_INT64 -10 3") shouldBe Right(SInt64(-3))
+        eval(e"DIV_INT64 -10 -3") shouldBe Right(SInt64(3))
+      }
+
       "throws an exception if it overflows" in {
         eval(e"DIV_INT64 $MaxInt64 -1") shouldBe Right(SInt64(-MaxInt64))
         eval(e"DIV_INT64 $MinInt64 -1") shouldBe a[Left[_, _]]
@@ -92,6 +99,15 @@ class SBuiltinTest extends AnyFreeSpec with Matchers with TableDrivenPropertyChe
       }
     }
 
+    "MOD_INT64" - {
+      "is remainder with respect to DIV_INT64, i.e. b*(a/b) + (a%b) == a" in {
+        eval(e"MOD_INT64 10 3") shouldBe Right(SInt64(1))
+        eval(e"MOD_INT64 10 -3") shouldBe Right(SInt64(1))
+        eval(e"MOD_INT64 -10 3") shouldBe Right(SInt64(-1))
+        eval(e"MOD_INT64 -10 -3") shouldBe Right(SInt64(-1))
+      }
+    }
+
     "EXP_INT64" - {
 
       "throws an exception if the exponent is negative" in {

diff --git a/daml-lf/spec/daml-lf-1.rst b/daml-lf/spec/daml-lf-1.rst
@@ -3692,7 +3692,8 @@ Int64 functions
 * ``DIV_INT64 : 'Int64' → 'Int64' → 'Int64'``
 
   Returns the quotient of division of the first integer by the second
-  one.  Throws an ``ArithmeticError`` exception
+  one.  Rounds toward 0 if the real quotient is not an integer.
+  Throws an ``ArithmeticError`` exception
   - if the second argument is ``0``, or
   - if the first argument is ``−2⁶³`` and the second  one is ``-1``.