[jiro-by-nori]

Closes #43.

What was wrong

Every filesystem program was a comparison of two different programs. The model's
files live in the boot heap (ruby-lean/RubyCore/Heap.lean §Virtual filesystem),
so File.read("/tmp/readme.txt") answered "hello\n" on the model side while
CRuby read whatever the host had at that path — usually nothing. Nothing in
either corpus mentioned File./Dir./IO., so the whole VFS surface was
validated by hand. The trailing-slash bug fixed in #42 is the kind of defect a
corpus of these programs would have caught.

The change

• difftest/vfs.py: the fixture the model boots with (v1), and a
  Materialized context that writes it to the real filesystem, restores it and
  can reset it. It refuses to materialize over an existing path (so a user's
  /tmp/readme.txt is never overwritten) and removes everything it created.
• runner.run_case: a case whose sidecar names a fixture ({"vfs": "v1"})
  materializes it for the case and restores it at the end, including on a
  harness error. An unknown fixture name is a harness_error, never a skip.
• control.CRubyRunner.run / run_deterministic: reset the fixture before
  every CRuby run, so a program's writes cannot leak into the second run of
  the determinism check. The SUT is handed the tree the control started from,
  not the control's last write.
• difftest/corpus/vfs/: tier 5 — five programs pinning the fixture's bytes and
  sizes, path resolution (., .., //, trailing slash), a write read back,
  and the descriptor form that is still gated. Sidecars carry {"vfs": "v1"}.
• difftest run --tier vfs --sut lean runs the corpus whole and owns its own
  verdict: a gate is allowed (the model's filesystem is built one step at a
  time, so a gated step is a coverage measurement, not a pass), but a
  disagreement, a control failure or an unusable fixture exits 1. There is no
  baseline to absorb a silent one.
• An empty corpus is an error (VfsError, exit 2), not a silent pass: with no
  baseline for this tier, a moved directory would otherwise report "the model
  and CRuby agree" having compared nothing.
• make conformance runs it (Makefile — one line in the conformance target,
  plus the comment above it; this file needs the owner's review and it is the
  only owner-owned file touched, no other changes are in it).
• docs/testing.md, difftest/README.md, difftest/corpus/vfs/README.md
  describe the fixture and the rules for writing a case. The difftest coverage
  baseline moves up with the new module and tests.

Test plan

• uv run difftest run --tier vfs --sut lean → 4 agree, 1 sut_unsupported
  (the descriptor program), 0 disagree; run twice, /tmp left as found.
• uv run difftest run --tier vfs --sut identity → 5 agree. CRuby against
  CRuby through the fixture is the harness's own smoke test: it would fail if
  materialization differed from the model's tree.
• Fabricated disagreement (Dir.exist?("/tmp/readme.txt"), which the model
  currently answers wrongly — filed separately) → exit 1 and the case is listed
  under unexpected; occupied fixture path → exit 1 with a message naming the
  path and the user's file untouched; missing sidecar → exit 2.
• No regression in the existing corpora through the refactored runner:
  replay corpus/tier3 → 57 agree, 13 gated, 0 disagree; run --tier regressions → 221 held, 1 gated, 0 regressed.
• DIFFTEST_NO_SKIPS=1 uv run pytest → 204 passed, 0 skipped (15 new tests);
  ruff check + ruff format --check clean; mkdocs build --strict clean;
  scripts/check-coverage.py OK at the raised baseline;
  make check-not-weakened → CHECKS NOT WEAKENED.
• Not run locally: the full make conformance/make check (this machine has no
  C toolchain, so make deps cannot install the pinned gems). CI runs it.

Found while writing the corpus (filed separately)

Dir.exist? answers File.exist?: Dir.exist?("/tmp/readme.txt") is true in
the model and false in CRuby. The new corpus caught it on the first run; the
fix is in RubyCore/Builtins/FS.lean and is not in this PR (a model change
needs the proof books, and this PR is the harness). The corpus case will land
with that fix.

---

Authored by Jiro, an autonomous agent (Nori sessions), on behalf of
@sam-xif. The code and this description were written by the agent.