[jiro-by-nori]

What was wrong

The prelude installed index on Enumerable:

module Enumerable
  # `Array#index` with a block is the same search (the blockless forms stay on
  # the builtin; the block form falls through to here).
  alias index find_index

CRuby defines #find_index on Enumerable and #index only on Array (as
Array#find_index), so every including class answered a call CRuby refuses:

expression	before	CRuby 4.0.5
(1..5).index(3)	2	NoMethodError: undefined method 'index' for an instance of Range
{a: 1}.index(1)	nil	NoMethodError: … for an instance of Hash
class C; include Enumerable; def each; yield 7; end; end then C.new.index(7)	0	NoMethodError: … for an instance of C

NoMethodError is inside the family the validator claims to exclude, so these
were wrong answers rather than gates — the inverse of the gated-miss work in
#27/#29/#31.

The change

ruby-lean/prelude/prelude.rb: the name moves onto class Array and the
Enumerable alias is deleted. Array#index is written out rather than aliased,
because the blockless forms have to keep answering:

• [1,2,3].index(2) is 1, [1,2,3].index { |x| x > 1 } is 1;
• two arguments raise CRuby's ArgumentError: wrong number of arguments (given 2, expected 0..1). The blockless builtin said expected 1, and the alias
  would have turned the same call into a gate;
• no argument and no block gates (it would need an Enumerator), as
  Enumerable#find_index already does, instead of raising that ArgumentError;
• the comparison is == on the element, and the array is read live, as
  rb_ary_index does;
• Enumerable#find_index is untouched, and Range#index and any user
  Enumerable now reach the ordinary miss path and raise CRuby's message.

One deliberate narrowing: rb_ary_index walks the array's own storage and never
calls each, but this body is Ruby and reads through each. A receiver that
defines each (a subclass or a singleton method) would therefore search
something CRuby never looks at, so it gates with Array#index on a receiver that defines #each instead of answering. No program in either corpus is affected.

Making Array#index a prelude definition also shadows the blockless
Array#index builtin (ruby-lean/RubyCore/Builtins/Collections.lean), which is
now unreachable; this PR leaves it in place so the model's boot heap, its guards
and the proofs over it are untouched. Removing the dead arm is a follow-up.

difftest/corpus/regressions/array-index-is-array-only.{rb,json} pins the whole
surface against CRuby 4.0.5, status fixed: the Array forms, the 0..1 arity
message, Range/Hash/user-Enumerable misses, Enumerable#find_index, ==
comparison and live reading.

Test plan

Run in this session against CRuby 4.0.5 (ruby 4.0.5p0) with Lean
v4.32.2. Nothing was weakened: no baseline file needed a new number.

Command	Result
make gen-check	all four generated sources fresh (the regenerated Prelude.lean / PreludeJson.lean are in this PR)
make books	Build completed successfully (1399 jobs) — every proof book, including the type-soundness theorem and its controls
make metatheory	builds; every audited theorem still rests on propext, Classical.choice, Quot.sound; the booted heap satisfies the assumptions the proofs make about it
make soundness	SOUNDNESS CHECK PASSED
make conformance	agree 1087 (baseline ≥1087), sut_unsupported 194 (≤194), not_compared 6 (≤6), disagree 0; regressions and tier 3 agree
make difftest-test	42 files, line 72.77% / branch 68.18% — COVERAGE OK
make desugar-test	agree: 1257 disagree: 0 out-of-fragment: 76, desugaring-rule coverage 76/76
make desugar-coverage	baseline: in-fragment=1211 (of 1282) current=1211 (of 1282)
desugar unit tests (by hand, see below)	917 runs, 0 failures, coverage 97.73% / 88.91% — COVERAGE OK
emitter unit tests (by hand, see below)	367 runs, 0 failures, coverage 98.17% / 82.33% — COVERAGE OK
make book-checks	FastPower: 72/72 inputs: CRuby, the model and the theorem agree
make feature-loading	three AGREE lines (require scope, re-entry, cache; throw/ensure; failed-load dependency)
make check-not-weakened	CHECKS NOT WEAKENED
make ci-sync, make prereqs	CI runs every make check target; every prerequisite present
ruff check . / ruff format --check .	clean; 114 files already formatted

Ad-hoc, before/after, with bin/ruby-lean --compare:

• before: (1..5).index(3) printed 2, {a: 1}.index(1) printed nil —
  DIFFER against CRuby;
• after: the new regression case and a probe of twelve Array#index shapes
  ([[1],[2]].index([2]), [1].index(1.0), [].index(1), a block that matches
  nothing, …) print identical output and exit AGREE.

Environment notes, so the numbers above are reproducible:

• the development bundle group needs json, whose native extension does not
  build against this box's zig cc (ld.lld: relocation R_X86_64_PC32 cannot be used against symbol '__cpu_model'), so bundle install ran with
  BUNDLE_WITHOUT=development and the two minitest suites were run with plain
  ruby -e 'Dir.glob(…)' plus the same scripts/check-coverage.py check;
• rubocop was installed outside the bundle and run over the whole tree
  (43 files inspected, no offenses detected). Neither ruby-lean/prelude/
  nor difftest/corpus/ is in RuboCop's Include list, so this change adds no
  lint surface;
• not run here: make comparator (fetches and rebuilds
  leanprover/comparator, and the theorem statement is unchanged) and
  make docs (mkdocs is not installed on this box and no documentation
  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.