[jiro-by-nori]

Summary

A File/Dir path argument containing a null byte is a wrong answer, not a gate. CRuby raises ArgumentError before touching the filesystem; the model answered a concrete value or false:

File.exist?("/tmp/a\0b")          # model: false   CRuby: ArgumentError
File.basename("/tmp/a\0b")        # model: "a\0b"  CRuby: ArgumentError
File.join("/tmp/a\0b", "z")       # model: "/tmp/a\0b/z"  CRuby: ArgumentError

The VFS step-1 builtins (File.exist?, File.file?, File.directory?, Dir.exist?) answered false, and the pure path helpers (File.basename, File.dirname, File.extname, File.join, and a File.basename suffix) answered a value. File.read/File.size/File.write happened to gate with a misleading "no such file" reason.

CRuby's messages are shape-specific, so the fix uses both:

• a path containing a null byte raises ArgumentError, "path name contains null byte";
• a File.join part or a File.basename suffix containing one raises ArgumentError, "string contains null byte".

ruby-lean/RubyCore/Builtins/FS.lean checks the path before any lookup (so read/size/write also answer the real error instead of a misleading gate). ruby-lean/prelude/prelude.rb checks the four pure helpers. The generated Prelude*.lean files are regenerated with make gen.

This is step-1 VFS correctness (umbrella issue #7). It is orthogonal to #85 (VFS differential corpus) and #87 (byte counts). No proof statements change; runFS_frame still builds because pushRootK leaves the heap unchanged.

Authored by Jiro, an autonomous agent — both this code and this description.

Test plan and validation

• Reproduced before the fix on main's model: the new regression program printed false\nfalse\nfalse\nfalse\n"a\\u0000b"\n"/tmp"\n""\n"/tmp/a\\u0000b/z"\n"abc" while CRuby printed twelve ArgumentError lines.
• Added difftest/corpus/regressions/file-path-null-byte.{rb,json}. It is a genuine DISAGREE on the old model and AGREE now (declared fixed, observed agree → held).
• uv run difftest run --tier regressions --sut lean: 220 cases, 219 agree, 1 pre-existing gate, 0 failures.
• Full tier-0 conformance over the harvested bootstraptest corpus: 1287 ran, 1087 agree, 194 gated, 6 not compared, 0 disagreements; scripts/check-conformance.sh prints CONFORMANCE OK.
• uv run difftest replay corpus/tier3 --sut lean: 57 agree, 13 gated, 0 disagreements.
• cd books && lake build: 1399 jobs, including runFS_frame.
• bash books/scripts/check-soundness.sh --proofs-only: SOUNDNESS CHECK PASSED.
• make gen-check: all four generated sources fresh. python3 scripts/check-not-weakened.py: CHECKS NOT WEAKENED.
• uv run pytest in difftest/: 158 passed; the 6 failures are the Sorbet tests, which cannot run here because the Sorbet gem is not installed (SorbetUnavailable), unrelated to this change.

Validation caveat: make check/make lint could not run end-to-end in this environment because Bundler cannot build the pinned json native gem. The lint configuration excludes ruby-lean/prelude/**/* and difftest/corpus/**/*, so this diff has no lint surface; the affected checks above were run individually.