bug: miscompilation in constant folding

[digama0]

This code is incorrect:

lean4/src/Lean/Compiler/ConstFolding.lean

Lines 50 to 53 in 8bbb015

	def getNumLit : Expr → Option Nat
	| Expr.lit (Literal.natVal n) => some n
	| Expr.app (Expr.const fn _) a => if isOfNat fn then getNumLit a else none
	| _ => none

lean4/src/Lean/Compiler/ConstFolding.lean

Lines 196 to 201 in 8bbb015

	def foldToNat (_ : Bool) (a : Expr) : Option Expr := do
	let n ← getNumLit a
	return mkRawNatLit n
	def uintFoldToNatFns : List (Name × UnFoldFn) :=
	numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat) :: r) []

It performs constant folding for UIntN.toNat using getNumLit, but getNumLit recognizes expressions like UIntN.ofNat M where M is larger than the bit size without performing modular reduction.

This results in a miscompilation / native_reduce proof of false:

theorem false : False := by
  have : (123456789012345678901).toUInt64.toNat = 123456789012345678901 := by native_decide
  simp [Nat.toUInt64] at this

Reported on Zulip.