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.
Implement issue #7 ship-order step 4: `File.open(path[, mode]) { |io| ... }` runs the block with the descriptor and closes it on normal return and every unwind (raise/break/return), returning the block's value. The non-block form is unchanged. The block form is a prelude method, not a builtin: a pure builtin cannot push a block frame, so closing on both paths needs a real yield inside begin/ensure/end (the same shape String#sub/#gsub use). The step-2 arm is renamed to an internal singleton primitive File#__open (registered as __open in PreludeBoot), and prelude.rb defines File.open on top of it, so path/mode allocation keeps one definition and unknown modes / missing paths gate byte-identically with and without a block. File#open leaves blockSensitiveBids, since `open` is now Ruby and `__open` is only reachable from the prelude. Evidence: RATCHET GREEN (256 agree, 0 disagree); check-isolation.sh OK; check-proofs.sh OK (standard axioms); Prelude.lean fresh under gen-check; model-vs-CRuby byte-for-byte on 14 block-form probes including exception, break/next/return, nested opens, and the write path.
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-step4-file-open-block
branch
from
October 10, 2026 04:04
8b81ceb to
414b5b3
Compare
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
Implements step 4 of the ship order in #7: block-form
File.open.The descriptor is closed on normal return and every unwind (raise,
break,return), exactly as CRuby does.Design
RubyCore/README.md§Mechanization), so "close on both paths" needs a realyieldinsidebegin … ensure … end— the same shapeString#sub/#gsubalready use.File#__open(registered__openinPreludeBoot.lean), andprelude.rbdefinesFile.openon top of it. Path/mode allocation keeps one definition; the prelude owns only the argument shape and theensure.File#openleavesblockSensitiveBids:openis now Ruby and__openis only reachable from the prelude, so nothing above the builtin needs to catch a stray block any more.File.open: mode q outside step 2, step-1 ENOENT).Changes
ruby-lean/RubyCore/Builtins/FS.lean—File#open→File#__open, with a comment recording the split.ruby-lean/RubyCore/Builtins/Support.lean— dropFile#openfromblockSensitiveBids.ruby-lean/RubyCore/PreludeBoot.lean— register the__opensingleton.ruby-lean/prelude/prelude.rb— theFile.openmethod.ruby-lean/RubyCore/Prelude.lean— regenerated.ruby-lean/notes/model/implementation-notes.md— step-4 record.Validation
RATCHET GREENfromscripts/run_typed_ratchet.sh(256 agree, 0 disagree).scripts/check-isolation.shOK (no new imports);scripts/check-proofs.shOK (standard axioms).gen-check:RubyCore/Prelude.leanfresh; desugar round-trip 46/46; difftest pytest 160 passed./tmp/readme.txtholding"hello\n"across 14 block-form probes: block read /read(2)/ sequentialread; the block value as a String, asnil, and viabreak/next/return; an exception in the block rescued outside with the descriptor observed closed; nestedFile.openblocks; the non-block form returning the descriptor; and the"w"path.The hermetic difftest
"vfs"fixture envelope remains the deferred step-1 follow-up (#8), so these probes are the direct CRuby comparison in its absence — the same approach steps 1–3 took.This PR was authored by Nori, an autonomous agent, including the code and this description.
Part of #7 (step 4 of the ship order). Stacked on
nori/vfs-step2-file-open(#26); it needs that step's descriptor builtin andPayload.io.