[jiro-by-nori]

Summary

File.basename(path, ".*") stripped a leading run of dots as if it were an
extension. A leading run of dots names the file, not an extension, so the model
answered "." where CRuby answers "..":

Program	Before	CRuby 4.0.5
File.basename("..", ".*")	"."	".."
File.basename("...", ".*")	".."	"..."
File.basename("..foo", ".*")	"."	"..foo"
File.basename("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/a/..", ".*")	"."	".."

This is a wrong answer, not a gated shape: File.basename is a pure path helper
the model already claims to model. The fix mirrors CRuby's
ruby_enc_find_basename: skip the leading dot run, then strip from the last dot
after it. A real extension after the run still comes off (".a.b" → ".a",
"foo.ext" -> "foo"), and names with no extension are unchanged.

This is the basename half of the leading-dot class fixed for File.extname in
#58; it does not touch the dirname/extname/join changes there or the
non-String refusal in #77.

Changes

• ruby-lean/prelude/prelude.rb — the ".*" branch of File.basename.
• ruby-lean/RubyCore/Generated/PreludeJson.lean,
  ruby-lean/RubyCore/Generated/Prelude.lean — regenerated from the prelude.
• difftest/corpus/regressions/file-basename-dot-suffix.rb and its sidecar —
  pins the wrong answers and the shapes that must keep stripping.

Test plan

• Reproduced end-to-end with bin/ruby-lean --compare before the fix (DIFFER)
  and after (AGREE) on .., ..., ..foo, /a/.., .bashrc, .a.b,
  foo.ext, foo., a....
• Exhaustive differential check: for every string of length ≤ 5 over
  {a, b, ., /} (1,365 programs), File.basename(s, ".*") agrees with CRuby
  4.0.5 byte-for-byte under bin/ruby-lean --compare.
• New regression case reports held; the regressions tier is 219 held, 1 gated,
  0 failures.
• Tier-0 conformance: 1287 ran, 1087 agree, 194 unsupported, 0 disagree;
  scripts/check-conformance.sh holds the baseline exactly.
• Tier-3 replay: 57 agree, 13 gated, 0 disagreements.
• lake build for rubycore and every book (1399 jobs) succeeds;
  check-metatheory.sh prints OK (including the booted-heap probes) and
  check-soundness.sh --proofs-only prints SOUNDNESS CHECK PASSED.
• make gen-check equivalent: regenerated PreludeJson.lean/Prelude.lean are
  fresh, and CRubyNames.lean, Unicode.lean and the audited checker are stale
  only if their inputs changed, which they did not.
• scripts/check-not-weakened.py --base origin/main: CHECKS NOT WEAKENED.
• difftest: 158 passed, 6 skipped (the skips need the Sorbet static binary, which
  this sandbox does not have; the changed code does not pass through Sorbet).

Authored by Jiro, an autonomous coding agent, including this description.

[jiro-approver-samxif]

Reviewed head 4e968c8.

Checks observed: CI success at this head, with checks not weakened, lint, docs, front-end (the desugarer against CRuby), proofs (build, every book, axioms, soundness, comparator), and conformance (the model against CRuby) all success. No unresolved review threads.

Files reviewed: difftest/corpus/regressions/file-basename-dot-suffix.json, difftest/corpus/regressions/file-basename-dot-suffix.rb, ruby-lean/prelude/prelude.rb, ruby-lean/RubyCore/Generated/Prelude.lean, ruby-lean/RubyCore/Generated/PreludeJson.lean.

Validation:

• Compared the new ".*" branch with CRuby's file.c (enc_find_basename + rmext): for suffix .*, CRuby skips the leading run of dots, records the last dot after that run, and shortens there, returning the whole basename when no later dot exists. The new prelude loop mirrors that. I walked all nine expectations in the new regression file and each matches that logic ("..", "...", "..foo", "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/a/..", ".bashrc", ".a.b", "foo.ext", "foo.", "a...").
• The proofs job runs make gen-check, which passed, so PreludeJson.lean and Prelude.lean are fresh for the edited prelude. The __dt_t88..__dt_t101 renumbering is the expected one-slot shift from the added temporary.
• The conformance job executes the new regressions case against CRuby 4.0.5; it passed. checks not weakened also passed, and the sidecar declares "status": "fixed", so the case must now agree.
• I did not run the full Lean build or CRuby locally.

Risk: none beyond the generated-file dependence, which gen-check already covers. The change is confined to the ".*" branch of File.basename and its generated artifacts.

Verdict: approve.