[sam-xif]

Summary

require_relative now resolves its argument against the running file's directory in the symbolic filesystem (VFS) and runs the pre-desugared body of the file it names. It previously gated (Require.lean "require_relative needs source-file resolution"). Plain require is unchanged — still the name-keyed modeled standard libraries; $LOAD_PATH-based require over the VFS is the next slice.

This is the first slice of M1 in a staged plan toward modeling require, the gem system and Marshal, so that deserialization gadget chains become ordinary, analyzable program traces. The plan is in ruby-lean/notes/model/marshal-require-gem-plan.md; this step is recorded in ruby-lean/notes/model/implementation-notes.md.

Stacked on #71 (generated Lean sources are build outputs, not committed): this PR's VfsFixture.lean/VfsFixtureJson.lean are generated and not committed either. Merge #71 first; GitHub then retargets this to main.

Design

The fixture, generated like the prelude. Every .rb under ruby-lean/prelude/vfs/ is mounted into the VFS as a regular file (its bytes) and desugared to a RubyCore Expr; the model never parses Ruby at run time. scripts/gen_vfs.rb writes the bodies as JSON plus raw bytes and pre-split path components (Generated/VfsFixtureJson.lean); genvfs decodes them to RubyCore terms (Generated/VfsFixture.lean): rawFiles, and requireBodies, each body keyed by its canonical path. Both come from the same source file in one generation step, so File.read of a library file and the body require_relative runs cannot drift. make regenerates both before the model builds.

Mounted by the boot, so it is in the booted-heap literal. Prelude.boot ends by mounting the files (Boot.mountFiles, ordinary heap writes). genbootedheap therefore writes them into Generated/BootedHeap.lean, boot_eq_booted compares them like the rest of the heap, and initWithPrelude = initOnBooted holds with no change to its proof: both start from that heap and set the same constant requireBodies. Nothing in Boot.initHeap moves.

Lookup by object, not by spelling. require_relative joins a relative argument onto the source file's directory, resolves it with the existing step-1 VFS.resolve (which already handles ./..), then runs the requireBodies entry whose canonical path resolves to the same object, caching under that path. Any spelling of a file (greeting, ./greeting, greeting.rb) loads once, as CRuby's realpath-keyed cache does. Re-entry and retry ride the existing requireK continuation.

Kernel-reducible boot. boot_eq_booted has the kernel run the boot. Json.parse (partial) and String.splitOn (well-founded recursion) do not reduce, so decoding happens in genvfs and components are split in the generator; the mount is a fold over literals.

Honest gates. A path that does not resolve, or resolves to a file with no modeled body, gates by name (CRuby raises LoadError; error classes are issue #7 step 7). require_relative with no source file (e.g. from eval) gates.

Proof fallout. notDone and framing lemmas for runLibraryBody/callRequireRelative, pushRootK_requireBodies for the new Machine field, and FastPower's two pinned object ids +5 (the mount allocates five objects before the program runs).

Verification

Locally, from regenerated sources (CRubyNames.lean/Unicode.lean taken from main, since they only regenerate identically on the pinned Ruby): make lean-exes; make books (every book); make feature-loading — model vs CRuby 4.0.5, byte-for-byte, on three new require_relative cases (load with a transitive require_relative; caching, where a repeat and an already-loaded file both return false; a circular pair seeing false mid-load; explicit .rb and ./ spellings loading once) alongside the existing require cases; axioms of the affected lemmas are the standard three; ruff and RuboCop clean. CI runs the full make check.

---

Authored by Claude (an agent). A human should review before merging.
🤖 Generated with Claude Code