[jiro-by-nori]

Problem

File.basename, File.dirname, File.extname and File.join coerced every path argument with to_s, so a program whose argument was not a String ran to a value where CRuby raises:

program	before	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.extname(:sym)	""	TypeError: no implicit conversion of Symbol into String
File.join(1, 2)	"1/2"	TypeError: no implicit conversion of Integer into String

AGENTS.md rule 3 says the model declines rather than approximates, so this is the wrong direction: a program outside the modeled domain answered instead of gating or raising.

The change

ruby-lean/prelude/prelude.rb only; the generated PreludeJson.lean / Prelude.lean follow.

• A path argument now goes through CRuby's FilePathValue (rb_get_path): a String stands, otherwise to_path and then to_str must answer a String, and anything else raises CRuby's byte-exact TypeError. The message names the converted value's class when a conversion answers a non-String, and nil / true / false for those immediates. An object whose class has no faithful name (an anonymous class prints a native address) gates with a named Unsupported instead of a message the model cannot reproduce.
• File.basename's suffix uses the narrower StringValue (String or to_str, never to_path), and an omitted suffix now differs from an explicit nil, which raises.
• File.join gained the rest of rb_file_join so the coercion change does not trade one wrong answer for another: nested arrays are joined to Strings first (join([[], []]) is "/", not ""), a cycle raises ArgumentError: recursive array, and the separator rule is CRuby's (join("a/", "/b") is "a/b", join("a//", "//b") keeps two — the model produced "a////b" for both before).

String arguments and the modeled Pathname (via to_path) answer exactly as before, and unmodeled File. class methods still gate through the prelude's method_missing.

Test plan

• New regression case difftest/corpus/regressions/file-path-argument-conversion.rb (sidecar status: "fixed"), run by make conformance's regressions tier: 49 rows covering the four defect rows, the immediate/class naming, to_path over to_str, a bad to_path result, to_s-only refusal, the suffix rules, the empty/nested-array cases, the separator rule and the recursive arrays.
• Exhaustive separator check outside the harness: all 819 one-, two- and three-element tuples of a nine-string separator alphabet, plus 374 nested-array/recursion/coercion cases, compared row-for-row against CRuby with zero disagreement.

Validation

Toolchain built for this run: Lean v4.32.2, CRuby 4.0.5, Python 3.12.

• make check → make check: ALL CHECKS PASSED (lint; generated sources fresh; the model; every proof book including the booted-heap metatheory, the soundness theorem and controls, and the comparator; the desugarer and emitter suites; difftest's own tests at their coverage baseline; conformance: ran 1287, agree 1087, sut_unsupported 194, not_compared 6, disagree 0 — exactly the recorded baseline, with the regressions and tier-3 tiers agreeing; feature-loading; the program books; the docs).
• make check-not-weakened → CHECKS NOT WEAKENED.

Fixes #57

---

Authored by Jiro, an autonomous agent (Nori sessions), including this description. Reviewed changes are welcome from @sam-xif.