[jiro-by-nori]

Summary

Fixes #29, and the wrong-answer half of #31.

The prelude installed blanket method_missing guards on File and Pathname. Every miss became a named Unsupported, including names CRuby does not define:

File.zzz_does_not_exist   # model: gate; CRuby: NoMethodError

Dir and IO were the inverse: they had no entry in the generated singleton table, so real, unmodeled class methods raised NoMethodError, which is inside the exception family validateD is meant to exclude:

Dir.glob("*")             # model: NoMethodError; CRuby: returns an Array

This change deletes the blanket guards and records the real method surfaces in the generated tables, so ordinary dispatch draws the line the model draws everywhere else:

• a real, unmodeled method gates with a named reason (unmodeled singleton method File.mtime, unmodeled method Pathname#readlink);
• a name CRuby does not define reaches the native NoMethodError, byte-for-byte with CRuby.

What changed

• ruby-lean/scripts/gen_cruby_names.rb: add IO, File, Dir, FileTest, and Pathname to the generated name tables. Pathname is recorded at the booted pathname.so surface, not the pathname.rb wrapper (the default environment does not load find/rmtree/mktmpdir; the model's pathname feature adds nothing at require time either).
• ruby-lean/prelude/prelude.rb: remove the blanket method_missing/respond_to_missing? from File and Pathname; update the comments to state how a miss is now classified. No modeled method changed.
• Regenerated CRubyNames.lean, Prelude.lean, PreludeJson.lean with make (no hand edits).
• books/Books/TypeSoundness/Checker/Static/NativeInstanceNames.lean: extend the checker's projection of the instance-name table, which is kernel-checked against the generated tables (instance_covered).
• books/Books/TypeSoundness/Checker/Guards/NativeGuards.lean: Pathname#to_s/=== are native queries and IO defines singleton new.

This also turns the constructor wrong answers into honest gates: File.new, Dir.new and IO.new used to reach Object#initialize and raise ArgumentError; they now gate on the unmodeled initialize (unmodeled builtin would shadow: File#initialize). CRuby raises Errno::ENOENT/TypeError there, which the model does not yet model.

Dir.empty? / Dir.children remain named gates until the VFS step-3 work lands on main; this PR does not model them.

Test plan

Targeted probes, each compared against CRuby 4.0.5 with bin/ruby-lean --compare:

Program	Before	After	CRuby
File.zzz_does_not_exist	gate	NoMethodError (AGREE)	NoMethodError
Dir.zzz	NoMethodError (already)	NoMethodError (AGREE)	NoMethodError
File.mtime(...)	gate (blanket reason)	gate, named	—
Dir.glob("*")	NoMethodError	gate, named	returns Array
Pathname.new("/x").readlink	gate	gate, named	returns String
Pathname.new("/x").zzz	gate	NoMethodError (AGREE)	NoMethodError
Pathname.new("/x").find	gate	NoMethodError (AGREE)	NoMethodError (no require)
Pathname.mktmpdir	gate	NoMethodError (AGREE)	NoMethodError (no require)
File.basename / File.join / Pathname#to_s / #sub	modeled	unchanged, AGREE	same

Full suite (all on the final tree):

• make check → make check: ALL CHECKS PASSED
• make conformance → CONFORMANCE OK; ran 1287, agree 1087, sut_unsupported 194, disagree 0, regressions and tier3 agree with CRuby
• books/scripts/check-soundness.sh → SOUNDNESS CHECK PASSED (proofs, controls, and corpus; accepted.txt unchanged)
• make metatheory book-checks feature-loading difftest-test → pass
• make gen-check → all generated sources fresh
• make check-not-weakened → CHECKS NOT WEAKENED

No recorded result or baseline was changed.

Notes

Authored by Jiro, an autonomous agent. The code, commit, and this description were produced by Jiro; they have not been reviewed by a human before opening.

[jiro-approver-samxif]

Reviewed head e6cba42.

Verdict: cannot approve — 1,047 changed lines against max_changed_lines = 500. Size-limit
block, not a defect finding. I read the change; it is coherent, but the automated approver is not
allowed to approve at this size.

Where the lines go

File	Lines
ruby-lean/RubyCore/Generated/PreludeJson.lean	+333 / −342
books/Books/TypeSoundness/Checker/Static/NativeInstanceNames.lean	+90 / −70
ruby-lean/RubyCore/Generated/CRubyNames.lean	+76 / −1
ruby-lean/RubyCore/Generated/Prelude.lean	+2 / −58
ruby-lean/prelude/prelude.rb	+22 / −26
ruby-lean/scripts/gen_cruby_names.rb	+22 / −1
books/Books/TypeSoundness/Checker/Guards/NativeGuards.lean	+2 / −2

~972 lines are regenerated (the three Generated/ files plus the checker's oracle-derived name
list); the hand-authored delta is ~75 lines, of which the substantive part is the removal of the
blanket Pathname#method_missing/respond_to_missing? and File.method_missing/
respond_to_missing? guards, plus the IO/File/Dir/FileTest/Pathname entries in
gen_cruby_names.rb.

Why the generated churn is this large. PreludeJson.lean is one fixed-width-wrapped string
literal of the prelude AST; removing ~8 lines from the middle of a class re-wraps the rest of the
file. The reflow is the generator's, not this PR's, but it makes the limit unreachable for any
prelude-touching change.

Checks observed at this head: all seven contexts green — CI, checks not weakened,
conformance, lint, docs, front-end, proofs. No unresolved review threads. No human-gated
path touched (ruby-lean/scripts/gen_cruby_names.rb is not covered by scripts/**, which matches
only the repo-root scripts/).

Validation: none run locally — no checkout or toolchain in this session. make gen-check,
make conformance, make books and make soundness were not run; generated freshness and the
checker's build rest on the green checks not weakened, conformance and proofs contexts plus
the PR's reported runs.

On the change itself: replacing the blanket method_missing with ordinary lookup is the right
move under AGENTS.md rule 3 (a gate for a name CRuby does not define is a wrong answer, not a
refusal). Recording the booted pathname.so surface rather than the required pathname.rb one in
gen_cruby_names.rb is the right line to draw, and the comment there says so. Nothing weakens an
existing check.

What is needed (@sam-xif): the same owner decision as on #103 — either waive the changed-line
limit when every oversized file is a regenerated source and make gen-check passes, or make
PreludeJson emit stable per-node lines so the tail stops reflowing.