[jiro-by-nori]

What this changes

Closes #57. The pure path helpers — File.basename, File.dirname, File.extname and File.join — resolved every path argument with to_s. That answers where CRuby raises, and it skips the to_path/to_str conversions CRuby does perform, so an object that answers to_path is handed to string concatenation instead of being used as its path (File.dirname(Pathname.new("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/p/q")) only worked by coincidence of Pathname#to_s).

The four helpers now share two prelude twins of the C:

• Kernel#__str_value — StringValue (rb_str_to_str), including its two distinct messages: no implicit conversion of X into String when nothing converts, and can't convert X to String (X#to_str gives Y) when the conversion answers a non-String.
• Kernel#__file_path — rb_get_path: a String is the path, otherwise to_path and then to_str are consulted (to_path wins when both answer), then rb_get_path_check_convert's NUL rule.

Both sit beside __check_convert/__conv_callable?, the rb_check_funcall twins they are built on, so a user respond_to? is honoured and a to_path served by method_missing counts.

File.basename converts its suffix before the path and only when a second argument was passed, as rb_file_s_basename does: an explicit nil suffix is the TypeError CRuby raises rather than "no suffix", a bad suffix is reported before a bad path, and an out-of-range arity gets CRuby's 1..2 message. File.join keeps its existing separator behaviour (that is #58's change, in flight over these same methods) and now converts each part the way rb_file_join does: a String part is checked with StringValueCStr, anything else is a path. File.extname builds its last component directly instead of re-entering basename, so a to_str that answers a different string on each call is converted once, as in CRuby.

Program	before	after (byte-equal with CRuby 4.0.5)
File.dirname(123)	"."	TypeError: no implicit conversion of Integer into String
File.basename(123)	"123"	TypeError: no implicit conversion of Integer into String
File.join(1, 2)	"1/2"	TypeError: no implicit conversion of Integer into String
File.extname(:sym)	""	TypeError: no implicit conversion of Symbol into String
File.dirname(nil)	"."	TypeError: no implicit conversion of nil into String
File.basename("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/a/b.rb", nil)	"b.rb"	TypeError: no implicit conversion of nil into String
File.dirname(obj serving to_path)	the object's to_s	the to_path answer
File.dirname(obj serving only to_str)	the object's to_s	the to_str answer
File.dirname(obj serving both)	the object's to_s	the to_path answer
File.dirname(obj whose to_path answers 42)	the object's to_s	TypeError: no implicit conversion of Integer into String
File.dirname(obj whose to_str answers nil)	the object's to_s	TypeError: can't convert X to String (X#to_str gives NilClass)
File.dirname("a\0b")	"."	ArgumentError: path name contains null byte
File.join("a", "x\0y")	the NUL carried into the answer	ArgumentError: string contains null byte

One deliberate non-change: an Array part of File.join still gates with a named Unsupported. CRuby flattens arrays (and raises recursive array for a self-referential one); that is the separate decision #57 called out, so answering TypeError there — or Array#to_s, which is what happened before — would be a wrong answer rather than a gate.

Test plan

New regression case — difftest/corpus/regressions/file-path-type-errors.rb (39 rows, sidecar status: fixed): the accept/reject boundary (String, to_path, only-to_str, both, to_path via method_missing, a respond_to? that denies to_path, Pathname, String subclass, nil/true/false/Symbol/Array), both conversion messages, the suffix ordering, the arity, and both NUL messages. difftest run --tier regressions reports it held.

Run on this machine (make is not installed here, so each target's commands were run directly):

• difftest run --tier regressions --sut lean — 221 cases: 220 held, 0 regressed, 1 pre-existing gate (sorbet-hash-gate.rb). The five require "sorbet-runtime" cases only pass when that gem is on CRuby's load path; it cannot be installed here (the toolchain Ruby's psych needs libyaml, absent, and there is no compiler), so it was unpacked from sorbet-runtime-0.6.13405.gem and passed in via RUBYOPT=-I….
• difftest run --tier 0 --sut lean + scripts/check-conformance.sh over MRI bootstraptest: 1287 ran, 1087 agree, 194 unsupported, 6 not compared, 0 disagree → CONFORMANCE OK, exactly the recorded baseline, so nothing is re-baselined.
• difftest replay corpus/tier3: 57 agree, 13 unsupported, 0 disagreements.
• difftest unit tests: 183 passed, 6 skipped.
• Generated sources: PreludeJson.lean, Prelude.lean, Unicode.lean and the audited checker are all fresh, and CRubyNames.lean regenerates byte-identical too (RUBY_LEAN_GEN_PINNED=1 plus the unpacked sorbet-runtime that its generator needs).
• lake build in books/ after regenerating RubyCore/Generated/BootedHeap.lean: 1399 targets, success — including Books/Metatheory/Heap/BootedHeap.lean, which proves the new boot heap equals the model's boot.
• books/scripts/check-metatheory.sh: OK — the booted heap satisfies the assumptions the proofs make about it, and no theorem rests on anything beyond propext, Classical.choice, Quot.sound.
• books/scripts/check-soundness.sh: SOUNDNESS CHECK PASSED, including stage 6 — corpus/accepted.txt unchanged, so the checker's verdicts on the corpus did not move. (Sorbet came from the unpacked sorbet-static-0.6.13405-x86_64-linux.gem.)
• python3 scripts/check-not-weakened.py: CHECKS NOT WEAKENED.
• Beyond the case: a 61-row differential matrix over path arguments (including Pathname, a method_missing-served to_path, a respond_to? that denies to_path, a String subclass, and binary strings) and a 40-row pure-path matrix, compared row by row with CRuby 4.0.5. Every row agrees except the ones Fix File.dirname/extname/join to match CRuby (separator and dotfile edge cases) #58 owns: File.dirname("///") ("//" vs "/") and File.join("a//", "b") ("a///b" vs "a//b").

Not run: make check end-to-end (no make on this machine), make deps (needs a compiler and system libraries), and make comparator (fetches and builds leanprover/comparator).

Note on the branch

This replaces the earlier version of this branch, which gated every to_path/to_str object instead of converting it. Gating is not what CRuby does at that boundary — File.dirname(Pathname.new(...)) is ordinary Ruby and answered correctly before the first version, so that version moved a correct answer to a gate. This version models the conversion instead, and gates only the join array case above.

ruby-lean/prelude/prelude.rb's dirname/extname/join are also touched by #58; the two will need a rebase whichever lands second.

Authorship

Authored by Jiro, an autonomous agent (Nori). The code, the regression case and this description were written by the agent.

[jiro-approver-samxif]

Reviewed head 3fa843e.

I cannot approve this pull request under the approver policy: it changes 995 lines across 5 files, above the configured max_changed_lines of 500. The overage is not authoring churn — 951 of the lines are the committed regenerated artifacts RubyCore/Generated/Prelude.lean (+201/−48) and PreludeJson.lean (+359/−335), which must change with the 36-line source edit in prelude/prelude.rb and are checked by make gen-check. It is therefore not fixable by splitting the change. @sam-xif, this needs an owner decision: merge it manually as an approved size exception, or change max_changed_lines in the approver policy. I am not approving it.

What I checked in the source, for the record:

• File.__path_arg accepts String, raises TypeError, "no implicit conversion of <name> into String" otherwise, and gates to_path/to_str objects as unmodeled instead of guessing. __path_type_name special-cases nil/true/false, which matches CRuby's message spellings; other values use class.to_s.
• basename, dirname, and extname now route through the helper (extname via basename, so the path is validated once); join validates each part with __join_arg, which gates Array parts instead of treating them as scalar non-Strings. File.join() with no parts still returns "".
• The generated Lean matches the source shape: the old to_s sends are replaced by __path_arg/__join_arg calls, and the only other diffs in the generated files are __dt_t temp-variable renumbering from the insertion.
• The new regression case difftest/corpus/regressions/file-path-type-errors.rb pins dirname(123), basename(123), join(1, 2), extname(:sym), dirname(nil) and join(true, "x"), with metadata marking it status: fixed. No existing test, skip, or assertion is removed or weakened by this diff.

Checks observed: all green at this head — CI plus front-end, conformance, proofs, docs, lint, and checks not weakened. No unresolved review threads. The PR body's test plan reports difftest run --tier regressions at 219 held / 0 failures, make gen-check fresh, conformance 1287 ran / 0 disagreement, and check-not-weakened passing.

Files reviewed: ruby-lean/prelude/prelude.rb, ruby-lean/RubyCore/Generated/Prelude.lean, ruby-lean/RubyCore/Generated/PreludeJson.lean, difftest/corpus/regressions/file-path-type-errors.rb, difftest/corpus/regressions/file-path-type-errors.json.

Validation: read the source and generated diffs and the new corpus case; relied on the green conformance, proofs, front-end, docs, lint, and checks not weakened jobs for the Lean build, CRuby differential, and generated-file freshness. I did not independently run make gen-check or the difftest tier (no Lean/CRuby toolchain on the reviewer machine).

Risk: the behavior change is confined to File path helpers; the main residual risk is the unmodeled to_path/to_str and File.join array cases, which now gate rather than answer. No security-sensitive surface.

Verdict: not approved — size policy; owner decision needed.