fix: bug at lean_nat_mod

fixes at #1433

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);

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

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