Repository navigation
Conversation
3 tasks
…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.
…(issue #27) A File object from File.open answered NoMethodError for every real File/IO instance method the model does not implement (path, fileno, eof?, binmode, reopen, stat, ...), where CRuby returns an ordinary value. NoMethodError is in the family the validator excludes, so File.open(p,"r").path was a wrong answer rather than an honest gap. Root cause: the VFS classes were added to the boot heap and their modeled methods installed, but IO/File/Dir were never added to the generated CRuby-name tables that Interp.crubyShadow walks on a lookup miss. The shadow never fired, so the miss reached the genuine-NoMethodError arm. Fix is data-only, reusing the existing shadow mechanism: - gen_cruby_names.rb FOLD gains IO/File/Dir, folding only the modules the L0 chain omits (File::Constants, Enumerable). IO is deliberately not folded into File (already in File's chain; folding it would spuriously gate File#close). - CRubyNames.lean regenerated (additive). - NativeInstanceNames.lean gains the 71 new selectors that NativePrefix.lean kernel-checks coverage of. - NativeGuards.nativeSingletonNew gains "IO" (CRuby's IO.new is a real singleton constructor, required by the singleton_covered theorem). Now File.open(p,"r").path gates as `unmodeled method IO#path`; an invented method (f.zzz) still raises NoMethodError; the modeled surface (File.read/size/exist?, IO#read/#read(n)/#close/#closed?) is unchanged. Evidence: run_clink_rebuild.sh CLINK REBUILD CHECKS PASS (125 certified, 0 gated, standard axioms); lake build rubycore active-ratchet green; check-isolation.sh OK; full run_typed_ratchet.sh identical to the pre-change baseline. Model-vs-CRuby 4.0.5 byte-exact on the modeled surface. Closes #27. Part of #7 (step 2 follow-up). Authored by Nori, an autonomous 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/fix-27-unmodeled-file-io-dir-gate
branch
from
October 10, 2026 04:04
2b1f22a to
65f1753
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
Fixes #27: a
Fileobject fromFile.openansweredNoMethodErrorfor every realFile/IOinstance method the model does not implement —path,fileno,eof?,binmode,reopen,stat, … — where CRuby returns an ordinary value.NoMethodErroris inside the type-error family the validator claims to exclude, soFile.open(p,"r").pathwas a wrong answer, not a gate.Found while landing step 2 of #7 (PR #26, on whose branch this stacks). Step 1 modeled
File/Dirsingleton methods and step 2 the descriptor I/O, but noFile/IOinstance method outside those surfaces was considered, and theIO/Fileclasses carried no refusal for the rest.Root cause
The VFS classes were added to the boot heap and their modeled methods installed, but
IO/File/Dirwere never added to the generated CRuby-name tables thatInterp.crubyShadowwalks on a lookup miss (RubyCore/CRubyNames.leanonly listed them asObjectconstants). The shadow never fired, so the miss fell through to the genuine-NoMethodErrorarm.Fix (data-only, reuses the existing shadow mechanism)
scripts/gen_cruby_names.rbFOLDgainsIO,File,Dir, folding in only the modules the L0 chain omits (File::Constants,Enumerable).IOis deliberately not folded intoFile— it is already inFile's model chain, and folding it would makecrubyClassDefines "File" "close"true and spuriously gate the modeledFile#close/#read, which resolve toIO.RubyCore/CRubyNames.leanregenerated (additive: 65 lines).Ratchet/Static/NativeInstanceNames.leangains the 71 new instance selectors thatDenote/Sem/Names/NativePrefix.leankernel-checks coverage of.Ratchet/Guards/NativeGuards.leannativeSingletonNewgains"IO": CRuby'sIO.newis a real singleton constructor, and thesingleton_coveredtheorem inDenote/Sem/Names/NativeGuards.leanrequires every singletonnewto be declared.Behaviour
File.open(p,"r").pathNoMethodError(wrong)unmodeled method IO#path(gate)"/tmp/readme.txt"File.open(p,"r").filenoNoMethodError(wrong)unmodeled method IO#fileno(gate)5File.open(p,"r").zzzNoMethodErrorNoMethodErrorNoMethodErrorFile.read(p)/IO#read/#read(n)/#close/#closed?Verification
scripts/run_clink_rebuild.sh→CLINK REBUILD CHECKS PASS(125 certified, 0 gated; standard axioms only).lake build rubycore active-ratchetgreen;scripts/check-isolation.shOK.scripts/run_typed_ratchet.shoutput is identical to the pre-change baseline (80/263 climbed, prefix 17, negatives 46/46, sameSorbet verdict movedset) — this sandbox has an unpinned Sorbet that makes the corpus stage red on the unmodified branch too, so the comparison is baseline-relative.File.read/size/exist?/file?/directory?/basename,File.open+read/read(n)/close/closed?); the listed unmodeled methods now gate instead of mis-raising.Notes
nori/vfs-step2-file-open, itself stacked on VFS step 1: File.read/write/exist?/file?/directory?/size over a boot fixture #21). Base branch set accordingly.File./Pathname#method_missinggates every unmodeled class method, including genuinely absent ones (File.zzz→Unsupportedwhere CRuby raisesNoMethodError). That asymmetry is pre-existing step-1 behaviour, not introduced here.Closes #27. Part of #7 (step-2 follow-up).
Authored by Nori, an autonomous agent.