[sam-xif]

Summary

Fixes #29 and #31: the prelude's blanket method_missing guards for File/Pathname (and the complete absence of one for Dir) answered every unmodeled call with a named Unsupported, including names CRuby does not define at all. That is a fidelity defect — a gate for a non-method — and Dir's real class methods (mkdir, glob, pwd, …) mis-raised NoMethodError, which is inside the type-error family the validator claims to exclude.

The model already draws the correct line in dispatch: a real unmodeled method gates (unmodeled singleton method File.mtime), an invented name reaches the native NoMethodError. It only lacked the data — the generated crubySingletonNames/crubyMethodNames tables had no entries for File, IO, Dir, FileTest or Pathname.

Stacked on #21 (VFS step 1). Base branch is nori/vfs-step1-file-read-write; the diff below is this fix only.

Closes: #29, #31.

What changed

Generator (ruby-lean/scripts/gen_cruby_names.rb)

• Add IO, File, Dir, FileTest, Pathname to FOLD so their real method names enter the dispatch-fidelity tables. File < IO, so inherited class methods (read/write/open) are found by the shadow's ancestor walk — no folding needed. Pathname is stdlib and CRuby 4.0 boots it, so require "pathname" makes the constant resolvable.

Generated (RubyCore/Generated/CRubyNames.lean)

• Regenerated with CRuby 4.0.5. The added classes contribute to crubyMethodNames, crubySingletonNames and crubyNamespaceConstants; every pre-existing entry is byte-for-byte unchanged.

Prelude (ruby-lean/prelude/prelude.rb)

• Remove Pathname#method_missing/#respond_to_missing? and File.method_missing/File.respond_to_missing?. Ordinary lookup now decides: real method → named Unsupported (via crubySingletonShadow/crubyShadow), invented name → native NoMethodError.

Checker projections (books/)

• NativeGuards.nativeQueryRows gains ("Pathname", ["===", "to_s"]) and nativeSingletonNew gains "IO".
• NativeInstanceNames.nativeInstanceNames gains the 142 instance-method names the new classes introduce, so NativePrefix's coverage proof still holds. The additions only make the checker refuse more names, never fewer — soundness is preserved.

Boot.lean: the comment that described the now-removed guard is corrected.

Before / after

Program	before	after	CRuby 4.0.5
File.zzz_does_not_exist	gate	NoMethodError: undefined method 'zzz_does_not_exist' for class File	same NoMethodError
File.mtime("/x")	gate File.mtime (only the pure path operations are modeled)	named gate unmodeled singleton method File.mtime	ordinary value
Pathname("/x").readlink	gate	named gate unmodeled method Pathname#readlink	ordinary value
Pathname.new("x").zzz	gate	NoMethodError: undefined method 'zzz' for an instance of Pathname	same NoMethodError
Dir.mkdir("/tmp/d")	NoMethodError: undefined method 'mkdir' for class Dir	named gate unmodeled singleton method Dir.mkdir	0 (creates it)
Dir.zzz_invented	NoMethodError	NoMethodError: undefined method 'zzz_invented' for class Dir	same NoMethodError

Test plan

Validated locally with a full toolchain built in this environment (Lean v4.32.2 from lean-toolchain; CRuby 4.0.5 core; the same generator pipeline CI uses):

• rubycore builds: lake build rubycore — success.
• Every affected proof builds with clean axioms: Books.TypeSoundness.Conformance.Names.NativePrefix, .Names.NativeGuards, .Class.ClassQueriesActual — the query_covered/singleton_covered proofs still hold after widening the tables; nativeQueryFreeB_sound depends on [propext, Quot.sound] as before.
• CRubyNames.lean is exactly what make gen-check will regenerate: I regenerated the core tables with a local CRuby 4.0.5 and confirmed (a) every pre-existing entry is byte-identical to the committed file and (b) the added entries are exactly the new classes'. The feature section is unchanged, byte-for-byte.
• PreludeJson.lean/Prelude.lean are fresh: regenerated with scripts/gen_prelude.rb + genprelude and cmp-equal to the committed files.
• No regression across the differential corpus's model outputs: ran all 219 programs in difftest/corpus/regressions/ through the model before and after this change; the observations are identical (0 differing files). The change only affects the invented-name branch the corpus never reaches.
• Differential check on the reproducers: every "after" row above matches CRuby 4.0.5's message byte-for-byte (verified with a local CRuby 4.0.5).

CI runs the full make check (conformance against CRuby, difftest, proofs, comparator) on this PR.

Notes

File.respond_to?(:mtime) now gates (it is a native singleton method), matching the model's existing rule for e.g. Integer.respond_to?(:sqrt), where CRuby answers true but the model declines rather than guess visibility. That is the model's documented choice, not a new behavior.