Repository navigation
Conversation
…fixture Implements the first shippable step of issue #7: the symbolic virtual filesystem. A file is a heap object (`Payload.file`/`Payload.dir`), the fixture is initial data H0' allocated at boot, path resolution is one pure total walk, and every unmodeled operation is a named Unsupported rather than a guess or a fabricated Errno. - New bootstrap classes IO, File < IO, Dir; new payload variants file/dir. - VFS.components/walk/resolve/lookup in Heap.lean; fixture allocated after main and the two realized eigenclasses, with `vfsBase` derived from `classTable.length` so new classes shift the fixture ids automatically. - Builtins/FS.lean: the six File operations plus IO.read/IO.write and Dir.exist?, discharged through the prelude's class-method path. File.write mutates inode bytes in place and returns the byte count; inspect/to_s of a raw file/dir object gate rather than guess CRuby's path-bearing rendering. - FS singleton methods are installed on their constants' eigenclasses in Prelude.boot (like Exception.exception), so they use ordinary dispatch and add no `send` special case. Only real CRuby class methods are installed, so Dir.read-style typos still NoMethodError exactly as CRuby does. - Repaired the boot-shift the new classes caused: intMetaId/strMetaId (prelude heap ids) 79/88 -> 87/96, ConstantReachControls' concrete heap/Next id, the runFS_frame/pathArg?/VFS.lookup root-frame lemmas, and bootGlobalConsts. Evidence: lake build rubycore + active-ratchet green, #guard bootOkB passes, run_typed_ratchet.sh prints RATCHET GREEN, check-proofs.sh passes, and the step-1 surface agrees with CRuby byte-for-byte. The hermetic difftest "vfs" envelope and un-gating the bootstraptest filesystem family (issue #8) are the next step. Authored by Nori (agent).
The first cut of `VFS.walk` treated `..` as a no-op, so
`File.read("/tmp/vfsdata/../readme.txt")` gated where CRuby answers. Store the
parent in the `dir` payload (root's is `none`) and climb it, which is the one
definition issue #7 asks for. `.`, `..`, `./c` and `a/b/../c` now agree with
CRuby byte-for-byte.
Authored by Nori (agent).
Add descriptors to the symbolic virtual filesystem of issue #7. A file is still a heap object; a descriptor is now one too. - Payload.io (inode, mode, pos, closed) and IOMode (read/write/append/ readWrite); each descriptor is its own object so per-descriptor position and closed-ness are observable, while the inode bytes stay shared. - File.open non-block, modes r/w/a/r+ (w truncates, a appends, r+ reads then overwrites at pos). IO#read (to EOF, or at most n, with the CRuby "" vs nil split), IO#write (byte count), IO#close, IO#closed?, IO#flush. - Class-object receivers keep the step-1 File.read/write and IO.read/write paths; .io receivers take the descriptor path. - File#open joins blockSensitiveBids: the block form (step 4) gates rather than silently running the block zero times. - Repr/Trace/nativeReprOwner gained the .io arm, still gating on rendering a descriptor (CRuby's File#inspect is path-bearing). - openIO allocates and mutates the heap, so runFS_frame needed a new openIO_frame lemma; it joins rootFrameLem and closes the same way. Missing path, closed stream, wrong-mode read, negative read length and the block form all gate with a named reason (Errno/IOError are step 7). Verified: lake build rubycore; RATCHET GREEN (run_typed_ratchet.sh, with and without RATCHET_SKIP_AGREEMENT=1); check-isolation.sh OK; check-proofs.sh OK (standard axioms). Model-vs-CRuby 4.0.5 byte-for-byte on a "hello\n" fixture for read/read(n)/read(0)/EOF, w-truncate, a-append, r+ read-then-write, and default mode.
…ach_line/pos/rewind) Step 5 of issue #7's ship order, over the step-2 descriptors. No new payload: every operation is a position move plus a slice of the inode's bytes. - IO#gets, all four CRuby forms: default "\n" separator, an Integer limit, a String separator, or both, plus gets(nil) reading to EOF. A separator runs through its first occurrence (whole remainder if absent), a limit truncates, and end of file answers nil. The surprising corner gets(0) = "" without moving the position, even at EOF, is modelled and pinned. - IO#pos reads the byte position; IO#pos= seeks (negative gates on the unmodeled Errno::EINVAL); IO#rewind returns the position to zero and answers 0. A closed descriptor gates on all three. - IO#readline and IO#each_line are prelude Ruby over gets, not primitives, so the block form is ordinary evaluation. readline's EOF case and the blockless each_line (CRuby answers an Enumerator a descriptor cannot build) gate by name rather than returning a guess. - ioId's builtin row gained readline/pos/pos=/rewind; gets and each_line were already listed by step 2 but unhandled, so they now resolve for real. No new proof lemma: gets/readline/pos=/rewind mutate the existing descriptor in place, the shape IO#read already had, so runFS_frame covers them. Verified: lake build rubycore/active-ratchet; CLINK REBUILD CHECKS PASS (125 certified, 0 gated, standard axioms); check-proofs.sh OK; check-isolation.sh OK; all 263 corpus programs still run with 0 hard failures. Model-vs-CRuby 4.0.5 byte-for-byte over the fixture /tmp/vfsdata/nums.txt for the gets/limit/separator matrix, pos, pos=, rewind, readline and block-form each_line. The full corpus gate (Sorbet pipeline) cannot run here because sorbet-static is absent (issue Authored by Nori (agent).
readline and each_line are prelude Ruby over gets, but the first cut took no
arguments, so readline("\n", 5) raised ArgumentError where CRuby answers and
each_line("2") gated. Both now take *args and forward them to gets, matching
CRuby's separator/limit arguments.
Verified: lake build rubycore/active-ratchet; model-vs-CRuby 4.0.5 byte-for-byte
for readline("2") and each_line("2") over /tmp/vfsdata/nums.txt.
Authored by Nori (agent).
getsArgsH's two-argument branch only accepted a String separator, so gets(nil, 3) gated where CRuby reads the rest capped at 3. nil as the first argument means "no separator" (read the remainder), and the limit still applies; getsLine already applies the limit after choosing the line, so only the argument parser needed the case. Verified: lake build rubycore/active-ratchet; model-vs-CRuby 4.0.5 byte-for-byte for gets(nil, 3), gets(nil, 100) and gets(nil). Authored by Nori (agent).
sam-xif
force-pushed
the
nori/vfs-step2-file-open
branch
from
October 10, 2026 04:04
07cd1c3 to
95f9811
Compare
sam-xif
force-pushed
the
nori/vfs-step5-gets-readline-pos
branch
from
October 10, 2026 04:04
17bf196 to
5472c23
Compare
This was referenced Oct 10, 2026
sam-xif
force-pushed
the
nori/vfs-step2-file-open
branch
from
October 10, 2026 15:17
95f9811 to
6d4f817
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Step 5 of #7's ship order (
gets/readline/each_line/pos/rewind), over the descriptors introduced in step 2 (#26). No new payload is needed: every operation is a descriptor position move plus a slice of the inode's bytes.IO#gets, all CRuby forms: default"\n"separator, an Integer limit, a String separator, or a separator plus limit,gets(nil)(read to EOF), andgets(nil, limit)(read the rest capped) — as well as the two-argumentgets(sep, limit). A separator runs through its first occurrence (whole remainder if absent), a limit truncates the line, and end of file answersnil. The surprising cornergets(0) = ""without moving the position, even at EOF, is modelled and pinned.IO#pos,IO#pos=(seeking; a negative offset gates on the unmodeledErrno::EINVAL), andIO#rewind(position to zero, answers0). A closed descriptor gates on all three.IO#readlineandIO#each_lineare written in the prelude, not as primitives, because each is defined overgetsand a block. Both take*argsand forward their separator/limit through togets.readline's EOF case raisesEOFError, and the blocklesseach_lineanswers anEnumerator— neither is modellable here (tracked by #37), so both gate by name rather than returning a guess. The block-formeach_line, which the slice actually uses, is exact.ioId'sbuiltinMethodsrow gainedreadline/pos/pos=/rewind;getsandeach_linewere already listed by step 2 but unhandled, so they now resolve for real.No new proof lemma is required:
gets/readline/pos=/rewindmutate the existing descriptor in place, which is the shapeIO#readalready had, so the step-2runFS_framecovers them.Verification
lake build rubycore validate-one active-ratchetgreen.scripts/run_typed_ratchet.sh --clink-rebuild→ CLINK REBUILD CHECKS PASS (125 certified, 0 gated; every theorem onpropext/Classical.choice/Quot.soundonly).scripts/check-proofs.sh→ metatheory builds, standard axioms only.scripts/check-isolation.sh→ OK./tmp/vfsdata/nums.txt("1\n2\n3\n"): the fullgetslimit/separator matrix (includinggets(nil, n)),pos,pos=,rewind,readline,readline("2"), block-formeach_line, andeach_line("2").Environment caveat: the full corpus gate (Sorbet → strip → desugar → emit) could not run here because the
sorbet-staticbinary is absent from this sandbox — the exact condition tracked by #32. The--clink-rebuildproof/control gate and the direct CRuby probes stand in; the change touches no checker rule.Follow-ups
readlineat EOF (needsEOFError/IOError/Errno::*, step 7) and blocklesseach_line(needs a descriptor-backedEnumerator).Base
Based on
nori/vfs-step2-file-open(#26) because step 5 needs the step-2 descriptors. Should be merged after #26.Authored by Nori, an agent, including this description.