[sam-xif]

Summary

The pure File path helpers modelled in the prelude (dirname/extname/join)
returned wrong answers for separator and dotfile edge cases. A wrong answer
is the worst kind of defect here — a silent disagreement with CRuby rather than a
named Unsupported — which AGENTS.md rule 3 ("The model declines; it does not
approximate") explicitly forbids. These helpers are the pure path operations that
issue #7 leaves in the prelude as Ruby string functions, and this restores their
CRuby fidelity.

Fixes, each derived from MRI's C source and verified byte-for-byte against
CRuby 4.0.5:

Program	before	CRuby	after
File.dirname("/foo/")	"/foo"	"/"	"/"
File.dirname("foo//bar")	"foo/"	"foo"	"foo"
File.dirname("foo//bar//baz")	"foo//bar/"	"foo//bar"	"foo//bar"
File.extname("..")	"."	""	""
File.join("a/", "/b")	"a///b"	"a/b"	"a/b"
File.join("a//", "/a")	"a////a"	"a/a"	"a/a"
File.join("a//", "a")	"a///a"	"a//a"	"a//a"

What changed

ruby-lean/prelude/prelude.rb (regenerated into RubyCore/Generated/Prelude*.lean):

• File.dirname now mirrors MRI's non-DOS rb_file_dirname_n for one level.
  The root of the bug was treating "text before the last /" as the answer, which
  keeps trailing and repeated separators. It now uses rb_enc_path_last_separator
  semantics — a trailing run of / does not name a component — so
  dirname("/foo/") is "/" and dirname("foo//bar") is "foo". The leading
  root is preserved ("//foo" keeps "//"), and "." is returned when the only
  separator is the path's own start.
• File.extname now skips a leading run of dots before finding the extension
  (MRI's ruby_enc_find_extname), so .bashrc/./../... have no extension
  while ".a.b" is ".b".
• File.join now mirrors MRI's rb_file_join: it collapses the separator it
  inserts with a leading / of the next part and drops trailing / from the
  accumulator when the next part is absolute, so join("a/", "/b") is "a/b".
  Interior separators are preserved (join("a//", "a") is "a//a").

Test plan

Validated locally with the full toolchain (Lean v4.32.2, CRuby 4.0.5, the
pinned Sorbet/uv environment), and by the repository's own checks:

• Model vs CRuby, exhaustively. Generated a 978-case corpus covering every
  dirname/extname/basename (with and without a suffix) edge case above plus
  every 2-part and 3-part combination of the separator alphabet
  ["", "a", "/a", "a/", "/a/", "//a", "a//", "/", "//"], and ran
  bin/ruby-lean --compare. All cases AGREE. The same corpus run against the
  unmodified prelude DIFFERs on 20+ lines, so the corpus distinguishes the fix
  from the defect.
• New regression guard. difftest/corpus/regressions/file-path-ops.rb (+
  sidecar, status: fixed) pins the fixed cases. Confirmed it reports
  outcome: regressed against the old prelude and held against this one, and
  that uv run difftest run --tier regressions --sut lean is green.
• make check → make check: ALL CHECKS PASSED, including:
  • make books — the model and every proof book build; the FastPower
    CRuby == model == theorem check runs 72/72.
  • make conformance — model vs CRuby over bootstraptest: 1287 ran, 0
    disagreement, baseline held.
  • make difftest-test — 147 passed.
  • make gen-check — all four generated sources fresh.
  • make docs — strict build clean.

Follow-up

Non-String path arguments are still coerced with to_s (so File.dirname(123)
answers "." where CRuby raises TypeError). Tracked separately in #57 — out of
scope here, which is strictly the separator/dotfile wrong answers.

Part of #7 (the pure path helpers it keeps in the prelude).

---

Authored by Jiro, an autonomous agent. I read the repository's AGENTS.md,
set up the full Lean + CRuby toolchain, derived the corrected semantics from
MRI's file.c (rb_file_join, rb_file_dirname_n, rb_enc_path_last_separator)
and ruby_enc_find_extname, and verified every change against CRuby 4.0.5 before
opening this PR.