Repository navigation
VFS step 1: a trailing slash or . after a non-directory is not that file - #42
Merged
Merged
Conversation
sam-xif
force-pushed
the
nori/vfs-step1-file-read-write
branch
from
October 10, 2026 04:04
2da15f8 to
1fc30e4
Compare
sam-xif
force-pushed
the
nori/vfs-trailing-slash-fix
branch
from
October 10, 2026 04:04
87906da to
9d742db
Compare
… file `VFS.components` dropped empty and `.` components, so `/tmp/readme.txt/` and `/tmp/readme.txt/.` had the same components as `/tmp/readme.txt` and `resolve` returned the regular file. CRuby requires the endpoint of a trailing slash, and the object `.` stands for, to be a directory: it answers `false` to `File.exist?`/`file?`/`directory?`, raises `Errno::ENOTDIR` from `File.read` and `Errno::EISDIR` from `File.write`. The model instead answered `true`/`true`/ `false`, read the file's bytes, and let `File.write` silently truncate it — a wrong answer rather than a gate, the failure mode issue #7's `File`/`Dir` guards exist to prevent. - `VFS.trailingSlash` (`path.length > 1 && path.endsWith "/"`) recovers the one signal `components` discarded; `resolve` now requires the endpoint to carry a `.dir` payload when it is set, else returns `none`. `/`, `//` and interior `//` are unaffected. - `components` keeps `.`; `walk` handles it explicitly (like `..`) by requiring the current object to be a directory before staying put, so `/tmp/readme.txt/.` fails as CRuby's does. The predicates now answer `false` and `File.read`/`write`/`open` fall through to their existing `VFS.lookup = none` named `Unsupported` (the `Errno` classes and message fidelity are step 7). `lookup` is still `Option ObjId` and the walk is still pure and total; no interface changed. Verified against CRuby 4.0.5 with the same fixture materialised: a 27-form path sweep over `exist?`/`file?`/`directory?` agrees on every line, and `File.read` is byte-exact where CRuby answers and a named gate where CRuby raises a step-7 `Errno`. `run_typed_ratchet.sh` is still GREEN (256 agree, 0 disagree, 125/125 clinks, 131/263 rungs). Authored by Nori (agent).
sam-xif
force-pushed
the
nori/vfs-trailing-slash-fix
branch
from
October 10, 2026 14:58
9d742db to
67d1d23
Compare
jiro-by-nori Bot
added a commit
that referenced
this pull request
Nov 10, 2026
Nothing exercised the model's filesystem against CRuby (issue #43). The model's files are boot-heap data, so a program that reads `/tmp/readme.txt` answers from the fixture on the model side and from whatever the host has on CRuby's side: the two were never the same program, and the whole VFS surface was validated by hand. The trailing-slash bug fixed in #42 is the kind of defect a corpus of these would have caught. A case now names its tree in its sidecar (`{"vfs": "v1"}`); `difftest/vfs.py` describes the tree the model boots with and materializes it before the case and restores it afterwards. Every CRuby run resets the tree first, so a program that writes still starts both runs of the determinism check from the same bytes, and the SUT is handed the tree the control started from rather than the control's last write. Materializing refuses if a fixture path already exists and restores everything it created, so the host's `/tmp` is never overwritten or departed from. The corpus is tier 5 (`difftest/corpus/vfs/`), run by `make conformance` with `difftest run --tier vfs --sut lean`. A gate is allowed there — the model's filesystem is built one step at a time, so a descriptor program gating is a coverage measurement, not a pass — but a disagreement, a control failure or an unusable fixture is not, and this tier owns that verdict rather than leaving it to a baseline. The first five programs pin the fixture's bytes and sizes, path resolution (`.`, `..`, `//`, trailing slash), a write read back, and the descriptor form that is still gated. Validation: `difftest run --tier vfs --sut lean` agrees on four programs and gates the descriptor one; `--sut identity` agrees on all five, which is the harness's own smoke test; the tier exits 1 on a fabricated disagreement and on an occupied fixture path, and leaves `/tmp` as it found it. `replay corpus/tier3` (70 programs) and `run --tier regressions` (222 programs) are unchanged: no disagreement, 221 held and one gated. `difftest/tests` passes in CI mode (204 passed, 0 skipped, including 15 new tests), `ruff check` and `ruff format --check` are clean, `mkdocs build --strict` passes, the difftest coverage baseline moves up (72.77/68.18 -> 73.27/68.67) and `make check-not-weakened` reports CHECKS NOT WEAKENED. The full `make conformance` target is left to CI: this machine has no C toolchain, so `make deps` (bundler and the pinned gems) cannot run here. Authored by Jiro, an autonomous agent (Nori sessions), on behalf of @sam-xif. Co-authored-by: Nori <contact@tilework.tech>
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
This PR fixes a wrong-answer bug in step 1 of issue #7 (the symbolic virtual filesystem, PR #21), found by running the step-1 surface against CRuby 4.0.5 with the same fixture materialised.
VFS.componentsdropped empty and.components, so/tmp/readme.txt/and/tmp/readme.txt/.produced the same components as/tmp/readme.txt, andVFS.resolvereturned the regular file for all three. CRuby requires the endpoint of a trailing slash — and the object.stands for — to be a directory:File.exist?("/tmp/readme.txt/")falsetruefalseFile.file?("/tmp/readme.txt/")falsetruefalseFile.directory?("/tmp/readme.txt/")falsefalsefalseFile.read("/tmp/readme.txt/")Errno::ENOTDIR"hello\n"UnsupportedFile.write("/tmp/readme.txt/", "x")Errno::EISDIRUnsupportedFile.exist?("/tmp/readme.txt/.")falsetruefalsetrue/"hello\n"where CRuby saysfalse/raises is exactly the wrong answer rather than a gate that issue #7'sFile/Dirguards exist to prevent (the predicate answers are modeled and must be byte-exact; the read/write errors areErrnoclasses, which are step 7, so they correctly fall through to a namedUnsupported).What changed
Two changes in
VFS(ruby-lean/RubyCore/Heap.lean), neither changing an interface —lookupstaysOption ObjIdand the walk stays pure and total:VFS.trailingSlash(path.length > 1 && path.endsWith "/") recovers the one signalcomponentsdiscarded.resolvenow requires the endpoint to carry a.dirpayload when that signal is set, else returnsnone./,//and interior//are unaffected (the root is a directory).componentskeeps., andwalkhandles it explicitly (like..) by requiring the current object to be a directory before staying put. This catches/tmp/readme.txt/., which CRuby also rejects.A new entry in
ruby-lean/notes/model/implementation-notes.mdrecords the bug, the fix and the evidence, and corrects the step-1 note that had summarised these as accepted "trailing-slash forms".Verification
CRuby 4.0.5 vs the model, same fixture (
/tmp/readme.txt="hello\n",/tmp/vfsdata/nums.txt="1\n2\n3\n") materialised for both:/,//, interior//,..,., leading/trailing slashes) overFile.exist?/file?/directory?now agrees with CRuby on every line.File.readon the same sweep is byte-exact wherever CRuby answers and a namedUnsupportedwherever CRuby raises a step-7Errno(no wrong answers remain).run_typed_ratchet.shis GREEN: 256 agree, 0 disagree, 125/125 clinks, 131/263 rungs — unchanged from the base branch.Base
Stacked on #21 (VFS step 1); base branch is
nori/vfs-step1-file-read-write, so the diff is this fix only. Should be merged after (or with) #21.This code and this description were authored by Nori, an autonomous agent.