[jiro-by-nori]

Authored by Jiro, an autonomous agent (Nori sessions), using the GitHub App.

Enumerable#take, #drop, #each_slice and #each_cons used their count or
size argument as it arrived — n <= 0 and then r.length == n — so each of
them answered where CRuby raises, and raised where CRuby answers. The count is
NUM2LONG in CRuby: an Integer, a Float truncated toward zero, or an object's
to_int, then a C long range check, then the method's own validation.

• __num2long in the prelude is that conversion, with CRuby's four messages.
  nil says no implicit conversion from nil to integer (lowercase, and "from"
  where every other object says "of X into Integer"), a to_int that answers a
  non-Integer names the answer (can't convert N to Integer (N#to_int gives NilClass)), an Integer beyond the range is bignum too big to convert into 'long', and NaN/±Infinity are float NaN / float Inf / float -Inf out of range of integer.
• take and drop convert first, then raise attempt to take negative size /
  attempt to drop negative size. Enumerable#first(n) delegates to take, so
  it inherits both.
• each_slice and each_cons convert their size and raise invalid slice size
  / invalid size, which also closes the two gates that stood where CRuby
  raises.
• A finite Float whose truncation is outside the long range still declines:
  CRuby prints that value at %.10g (float 9.223372037e+18 out of range of integer), a format this model cannot render, so it declines rather than guess
  the digits.

The generated PreludeJson.lean/Prelude.lean are regenerated from the prelude
by the build, not edited.

Diff size is dominated by the generated prelude sources: the hand-written change
is 77 lines of ruby-lean/prelude/prelude.rb.

Test plan

Run with CRuby 4.0.5, Lean v4.32.2, Sorbet 0.6.13405:

• make lean — the model, the regenerated prelude and the booted heap build.
• make conformance — over all 1287 bootstraptest programs: ran 1287,
  agree 1087, sut_unsupported 194, not_compared 6, disagree 0;
  CONFORMANCE OK. The recorded baseline is unchanged (no verdict moved).
• The regressions tier, over all 223 minimized cases: 222 held, 1 gated (gated
  before this change), no failures. The new case is enumerable-count-conversion.
• replay corpus/tier3 — 70 programs, 57 agree, 13 out-of-fragment, 0 disagree.
• make books — 1399 jobs, every proof book and the checker build.
• make metatheory — the metatheory audit passes and the booted heap satisfies
  the assumptions the proofs make about it.
• books/scripts/check-soundness.sh — SOUNDNESS CHECK PASSED, including the
  corpus run and the corpus/accepted.txt comparison (unchanged).
• difftest pytest with coverage — 189 passed, line 72.77% / branch 68.18%,
  COVERAGE OK.
• desugar/bin/run over the corpus — agree 1257 disagree 0 out-of-fragment 76 harness-error 0; desugar/bin/coverage holds its baseline (1211 of 1282).
• ruff format --check / ruff check — clean; make docs — clean;
  scripts/check-not-weakened.py --base origin/main — CHECKS NOT WEAKENED.
• Spot checks with bin/ruby-lean --compare, each now identical to CRuby
  including class and message: take(-1), take(0), take(1.5),
  take(-0.5), drop(-1), drop(2.9), take(nil), take(:a), take("2"),
  take(2**63), take(-2**64), take(2**63 - 1), take(Float::NAN),
  take(Float::INFINITY), take(-Float::INFINITY), an object whose to_int
  answers an Integer / nil / a Float, each_slice(1.5), each_cons(1.5),
  each_slice(0), each_cons(-2), {a: 1}.first(-1), (1..4).drop(2.5), and
  the same calls on a user Enumerable.

make lint's RuboCop stage could not run in this session (the json gem in the
Gemfile needs a C extension and the session has no compiler); it does not lint
the prelude or the corpora, so the change adds nothing for it to inspect.

Note for the maintainer

Enumerable#min_by(n) and #max_by(n) still answer
ArgumentError: wrong number of arguments (given 1, expected 0) where CRuby
answers the first/last n by key. That is a separate gap in the same file and is
not touched here.

Closes #137.