Miscompilation of UInt64.modn

[TwoFX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The code

lean4/src/runtime/object.cpp

Lines 1559 to 1562 in 174a5f3

	extern "C" LEAN_EXPORT uint64 lean_uint64_big_modn(uint64 a1, b_lean_obj_arg) {
	// TODO(Leo)
	return a1;
	}

fails if the second argument is large.

theorem false : False :=
  have : (UInt64.ofNat (2^64-1))%(2^63 : Nat) = 18446744073709551615 := by native_decide
  absurd this (by decide)

-- 'false' depends on axioms: [Lean.ofReduceBool]
#print axioms false

Expected behavior: Proof should be rejected.

Actual behavior: Proof is accepted.

Versions

4.11.0, 4.13.0-rc3, 4.12.0-nightly-2024-10-22, all on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.