[sam-xif]

Summary

IO#read(0) — a descriptor read with an explicit zero length — answered nil at end of file, where CRuby answers "". This is a wrong answer, not a refusal: CRuby's io_read returns an empty String for a zero length before it ever consults the stream for data.

io.c (io_read):

len = NUM2LEN(length);
if (len < 0) { rb_raise(rb_eArgError, "negative length %"PRIdLEN" given", len); }
...
rb_io_check_byte_readable(fptr);
if (len == 0) { io_set_read_length(str, 0, shrinkable); return str; }   /* "" */
...
n = io_fread(str, 0, len, fptr);
if (n == 0) return Qnil;                                                /* nil, only n > 0 */

So the len == 0 early return precedes the if (n == 0) return Qnil; EOF check. The step-2 descriptor read collapsed both cases into "no bytes available → nil", so read(0) at (or past) end of file disagreed with CRuby. The fix returns an empty String (with the inode's encoding tag) for n == 0, leaving the descriptor position untouched, and keeps nil for n > 0 at end of file. read(0) at the start of a stream already answered ""; only the EOF case was wrong.

This is part of #7 (VFS step 2, PR #26), which introduces IO#read. The fix is behaviour-preserving for every other shape.

What changed

ruby-lean/RubyCore/Builtins/FS.lean, IO#read, the [Integer n] branch: a new if n == 0 then okStrEnc m (h.get inode).binary "" case ahead of the existing avail == 0 → nil branch.

Test plan (how I validated)

I cannot run CRuby in this environment (no C toolchain / no buildable CRuby), so validation is twofold:

1. CRuby semantics from source. The behaviour is read directly from ruby/ruby io.c io_read (the snippet above): zero length returns "" regardless of EOF, before any read is attempted.

2. The model itself, byte-for-byte on the built rubycore. I built the model on this branch (lake build rubycore) and drove it with hand-written core-language programs over the boot fixture (/tmp/vfsdata/nums.txt = "1\n2\n3\n"):

   Program	This branch	CRuby
   io.read; io.read(0) (at EOF)	""	""
   io.read(0) (at start)	""	""
   io.read(3)	"1\n2"	"1\n2"
   io.read(100); io.read(1) (at EOF)	nil	nil
   io.read (to EOF)	"1\n2\n3\n"	"1\n2\n3\n"

   Before the change, the first row returned nil.

3. Proofs unaffected. lake build in books/ builds all 1396 targets with the change; every theorem still rests on propext + Classical.choice + Quot.sound.

Stacking

Based on nori/vfs-step2-file-open (PR #26), where IO#read is introduced. It applies cleanly to nori/vfs-step5-gets-readline-pos (PR #36) and I verified the same behaviour there after applying the patch — step 5 inherits the fix on rebase/merge.

Follow-up

A separate issue is filed for IO#gets/readline/each_line ignoring the global input record separator $/ (a related wrong answer in the same step-5 code, out of scope here).

---

Authored by Jiro, an autonomous agent. The code and this description were produced by an agent; the analysis above is from CRuby's io.c and the model's own observable behaviour.