From 386b0a75bcbccb2934cdc58d7d447b0e302865d1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 6 Aug 2022 08:03:27 -0700
Subject: [PATCH] fix: bug at `lean_nat_mod`

fixes at #1433
---
 src/runtime/object.cpp            |  2 +-
 tests/lean/1433.lean              | 18 ++++++++++++++++++
 tests/lean/1433.lean.expected.out |  6 ++++++
 3 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/1433.lean
 create mode 100644 tests/lean/1433.lean.expected.out

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 4d837a6afb..613060542e 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1112,7 +1112,7 @@ extern "C" LEAN_EXPORT object * lean_nat_big_mod(object * a1, object * a2) {
             lean_inc(a1);
             return a1;
         } else {
-            return lean_box((mpz_value(a1) % mpz::of_size_t(n2)).get_unsigned_int());
+            return mpz_to_nat(mpz_value(a1) % mpz::of_size_t(n2));
         }
     } else {
         lean_assert(mpz_value(a2) != 0);
diff --git a/tests/lean/1433.lean b/tests/lean/1433.lean
new file mode 100644
index 0000000000..3dec7cc651
--- /dev/null
+++ b/tests/lean/1433.lean
@@ -0,0 +1,18 @@
+def dividend := 2^65
+def divisor := 2^33+1
+
+def correctQuot := 2^32-1
+def correctRem := 2^32+1
+def wrongRem := 1
+
+theorem correct₁ : dividend / divisor = correctQuot := rfl
+theorem correct₂ : dividend = divisor * correctQuot + correctRem := rfl
+
+theorem wrong : dividend % divisor = wrongRem := rfl
+
+theorem unsound : False := by
+  have : wrongRem = correctRem := by
+    have h := Nat.div_add_mod dividend divisor
+    rw [wrong, correct₁, correct₂] at h
+    apply Nat.add_left_cancel h
+  contradiction
diff --git a/tests/lean/1433.lean.expected.out b/tests/lean/1433.lean.expected.out
new file mode 100644
index 0000000000..433c07cc71
--- /dev/null
+++ b/tests/lean/1433.lean.expected.out
@@ -0,0 +1,6 @@
+1433.lean:11:49-11:52: error: type mismatch
+  rfl
+has type
+  dividend % divisor = dividend % divisor : Prop
+but is expected to have type
+  dividend % divisor = wrongRem : Prop