Skip to content

Range#first answers its counted form and refuses a beginless range - #117

Open
jiro-by-nori[bot] wants to merge 1 commit into
mainfrom
range-first-counted
Open

jiro-by-nori[bot] wants to merge 1 commit into
mainfrom
range-first-counted

Conversation

@jiro-by-nori

@jiro-by-nori jiro-by-nori Bot commented Nov 9, 2026

Copy link
Copy Markdown
Contributor

Fixes #114.

Authored by Jiro, an autonomous agent (Nori sessions) on behalf of @sam-xif.

What was wrong

Range#first was a native builtin with arity 0, registered next to Range#begin
and sitting in zeroArgBids. Two of CRuby's three shapes were therefore wrong,
in opposite directions:

expression model before CRuby 4.0.5
(1..5).first(2) ArgumentError: wrong number of arguments (given 1, expected 0) [1, 2]
(1...5).first(9) ArgumentError (given 1, expected 0) [1, 2, 3, 4]
(1..).first(2) ArgumentError (given 1, expected 0) [1, 2]
(1..5).first(1, 2) ArgumentError (given 2, expected 0) ArgumentError (given 2, expected 1)
(nil..5).first nil RangeError: cannot get the first element of beginless range
(nil..5).first(2) ArgumentError (given 1, expected 0) same RangeError

The counted forms are a wrong ArgumentError — inside the family the validator
claims to exclude — and the bare form on a beginless range is a wrong answer,
not a gate. Range#last had the same defect (#110); Array#first(n) and
Array#last(n) already follow CRuby.

The fix

Range#first is now a prelude method in ruby-lean/prelude/prelude.rb, the same
treatment #size/#each/#cover? get and the same shape the #last fix takes:

  • the bare form answers #begin, after the beginless check;
  • the counted form is Enumerable#first(n): it stops at the end of the range,
    so an over-large n is the whole range and an endless range simply yields n
    elements;
  • the beginless check comes first, before the arity and count checks, because
    that is the order in rb_range_first — so a beginless range raises the same
    RangeError for every argument shape;
  • the count follows NUM2LONG and rb_ary_new2: a negative count is
    ArgumentError: negative array size (or size too big), and a count beyond a
    machine word either way is RangeError: bignum too big to convert into 'long';
  • a non-Integer count, or a range whose endpoints are not Integers, gates
    with a named Unsupported rather than guessing CRuby's per-class each
    TypeError (can't iterate from Float, no implicit conversion of String into Integer, …). Those are the only shapes this PR declines.

Range#begin keeps its own arity: (1..5).begin(0) is still
ArgumentError (given 1, expected 0), and the regression case pins it.

Test plan

Ran on Debian with Lean v4.32.2, CRuby 4.0.5 and the pinned Sorbet gems.

  • make check — make check: ALL CHECKS PASSED: make lint, gen-check,
    lean, books (every proof book, the checker included), metatheory (axiom
    audit), soundness (SOUNDNESS CHECK PASSED), comparator
    (Your solution is okay!), desugar-unit, emitter-unit, desugar-test,
    desugar-coverage, difftest-test, conformance, feature-loading,
    book-checks (72/72), docs.
  • make check-not-weakened — CHECKS NOT WEAKENED.
  • make conformance — 1287 ran, 1087 agree / 0 disagree / 194 unsupported,
    exactly the recorded baseline (difftest/coverage-baseline.json is unmoved).
    The regressions and tier-3 corpora agree.
  • The new difftest/corpus/regressions/range-first-counted.rb (status fixed,
    28 labelled cases) is reported held by
    uv run difftest run --tier regressions --sut lean, which went from 220 to
    221 held cases with 0 failures.
  • bin/ruby-lean --compare difftest/corpus/regressions/range-first-counted.rb
    — AGREE after the change. On origin/main's prelude the same command
    reports DIFFER, and the model's stdout is the wrong-arity
    ArgumentError on every counted case plus beginless: nil.
  • Probed beyond the corpus case: 28 further expressions (inclusive/exclusive,
    endless, descending, empty, single-element and negative ranges; n of 0, 5, 6
    and 9; bignum counts) all print byte-identical output to CRuby, and the seven
    gated shapes print the named Unsupported reason (exit 3) instead of an
    answer.

Not in this PR

Range#last's counted form is #110 (its own PR). Two defects found while
probing Range#first are filed separately rather than scope-crept in:
#115 (Range#count is aliased to #size, so a block is silently ignored and the
item argument is rejected) and #116 (Enumerable#index is invented, so
Range#index answers where CRuby raises NoMethodError).

The bare form is `#begin`, and a beginless range has no first element: CRuby
raises `RangeError` there, before it even scans the arguments. The counted
form is `Enumerable#first(n)`, so an over-large count is the whole range and
an endless range still answers; the count follows `NUM2LONG` (a negative count
is `rb_ary_new2`'s ArgumentError, one beyond a machine word its RangeError).

A non-Integer count, or a range with non-Integer endpoints, gates with a named
reason instead of guessing CRuby's per-class `each` TypeError.

Co-authored-by: Nori <contact@tilework.tech>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Range#first answers a wrong-arity ArgumentError for the counted form, and nil for the bare form on a beginless range

0 participants