[jiro-by-nori]

What was wrong

ruby-lean/prelude/prelude.rb's Kernel#__integer asked to_str before everything
else, in both of CRuby's forms, so an object defining both conversions converted
through its String:

expression	before	CRuby 4.0.5
Integer(Both.new) where to_int is 7, to_str is "42"	42	7
Integer(BothBad.new) where to_str is "zz"	ArgumentError: invalid value for Integer(): #<BothBad:0x…>	7
Integer(BothBad.new, exception: false)	nil	7

rb_convert_to_integer (object.c) has two arms: with a base it is
rb_check_string_type alone, and a non-String is refused ("base specified for non
string value"); without one it is rb_check_to_int, then rb_check_string_type,
then to_i. The model's order was "String first" in both.

The change

ruby-lean/prelude/prelude.rb:

• The probes run in rb_convert_to_integer's order. A String (including a subclass
  that defines to_int) is still type-tested first, as CRuby type-tests before
  calling anything.
• Integer(StrBad.new) names the converted String (invalid value for Integer(): "zz"), not the object: __parse_int is handed the String being parsed.
• String.try_convert does the rb_check_string_type conversion instead of the
  lenient __check_convert, so a to_str that answers a non-String is CRuby's
  TypeError: can't convert C to String (C#to_str gives Integer).

Three more rules of the same function were wrong on the same lines, and the
reordering walks straight through them, so they are fixed in the same commit:

• rb_protect(rb_check_to_int) swallows the to_int probe's exception — of any
  class, not just StandardError — and converts on. So Integer(obj) with a
  raising to_int and a to_i answers from to_i instead of raising. Without
  this, the new order would have regressed a method_missing that serves only
  to_str.
• exception: false is raise_exception, not a rescue around the whole
  conversion. A bad literal is nil, but rb_check_string_type and the radix check
  raise either way, and in the non-raising form the to_i probe is protected too
  (Integer(obj_with_raising_to_i, exception: false) is nil). It is threaded
  through __integer/__to_integer/__parse_int rather than rescued, so the arms
  cannot swallow each other's errors.
• invalid_integer's naming, as above.

Integer(Float::NAN) / Integer(Float::INFINITY) still decline (FloatDomainError
is not a modeled class), except under exception: false, where CRuby answers nil
and so the model now does too.

The regression case

difftest/corpus/regressions/integer-conversion-order.{rb,json}, status fixed,
pins the whole table against CRuby 4.0.5: the two probe orders, the raising-to_int
arms, the exception: false matrix (nil, raise-either-way, protected to_i), the
message naming, and the unchanged base-0 grammar plus base rejection.

Test plan

Every command below was run in this session against CRuby 4.0.5 (ruby 4.0.5p0) and
Lean v4.32.2, on a clean clone of main with this branch applied.

Command	Result
make conformance	ran 1287, agree 1087 (= baseline), sut_unsupported 194 (≤194), not_compared 6 (≤6), disagree 0; CONFORMANCE OK; regressions and tier 3 agree
cd difftest && uv run difftest run --tier regressions --sut lean	held 223 (including the new case), gated 1 (pre-existing), failures 0
make books	Build completed successfully (1405 jobs)
make metatheory	builds; every audited theorem still rests on propext, Classical.choice, Quot.sound; the booted heap satisfies the assumptions
make soundness	SOUNDNESS CHECK PASSED
make gen-check	all four generated sources fresh (the regenerated PreludeJson.lean / Prelude.lean are in this PR)
make difftest-test	201 passed; coverage line 73.19% / branch 68.61% — COVERAGE OK
make feature-loading	three AGREE lines
make book-checks	FastPower 72/72 inputs: CRuby, the model and the theorem agree; LoopSum agrees
make ci-sync	OK: CI runs every target of make check
make check-not-weakened	CHECKS NOT WEAKENED
lint by hand: rubocop 1.92.0, ruff 0.17.0, shellcheck, actionlint	clean; 44 files inspected, no offenses detected

Beyond the pinned case, before/after probes of ~90 shapes through
bin/ruby-lean --compare: 34 Integer program shapes (both probe orders, both
exception: modes, base 0/16/8/99/-2, to_int/to_str/to_i answering non-Integer,
answering nil, and raising) now print identical output and end identically; before
the change the first one disagreed on 8 of its 12 lines.

Known, pre-existing, and not addressed here (all reproduced before this change,
none made worse by it): a method_missing that defers with super still escapes
from __conv_callable? (that is #152 / #157), Integer(x, nil) does not raise
CRuby's no implicit conversion from nil to integer (the model cannot tell the
argument from an omitted base), and a non-boolean exception: is not refused.

Not run here: make comparator (fetches and rebuilds leanprover/comparator; no
theorem statement changes and make books builds every book), make docs (mkdocs
is not installed; no documented behaviour changed), and make desugar-unit /
make emitter-unit (their gems sit behind json, whose native extension this
sandbox has no C compiler for; no desugarer or emitter file changed).

---

Authored by Jiro, an autonomous coding agent, on behalf of @sam-xif. The code,
the regression case and this description were written by an agent; every result
above was produced by running the commands shown in this session.