Skip to content

VFS step 1: File.read/write/exist?/file?/directory?/size over a boot fixture - #21

Merged
sam-xif merged 2 commits into
mainfrom
nori/vfs-step1-file-read-write
Oct 10, 2026
Merged

VFS step 1: File.read/write/exist?/file?/directory?/size over a boot fixture#21
sam-xif merged 2 commits into
mainfrom
nori/vfs-step1-file-read-write

Conversation

@sam-xif

@sam-xif sam-xif commented Oct 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Summary

Implements step 1 of issue #7 — the symbolic virtual filesystem — which is the first shippable slice of that ship order ("step 1 alone is a complete feature"). A file is a heap object, the fixture is initial data, path resolution is one pure total walk, and an unmodeled operation is a named Unsupported.

Closes: part of #7 (step 1). Follow-ups for the remaining ship-order steps are listed below.

What changed

Model (RubyCore/)

  • Payload.file (bytes) / Payload.dir (entries) (parent) (Heap.lean). A directory is distinguished by payload, never a string convention; dir stores ordered (basename × ObjId) children plus a parent, so ./.., relative-path walking and listing share one definition.
  • Bootstrap classes IO, File < IO, Dir, appended after yielderId. mainId 44 → 47.
  • Fixture H₀′: five objects allocated after main and the two realized eigenclasses. vfsBase is derived (classTable.length + 3), so a new bootstrap class shifts the fixture ids without a second edit.
  • VFS.components / walk / resolve / lookup: one pure, total resolution from the fixture root. .. climbs the stored parent (root stays put), matching CRuby on a/b/../c, ./c and trailing-slash forms; only absolute paths resolve at step 1 (the cwd is Proposal: virtual filesystem with symbolic and dynamic modes for the Ruby semantics #7 open question 2).
  • Builtins/FS.lean: File.read/write/exist?/file?/directory?/size, plus IO.read/IO.write and Dir.exist?. Missing path, directory passed to read/size, non-String path, and any other shape return a named Unsupported — nothing guesses, nothing fabricates an Errno (classes/messages are step 7). File.write mutates inode bytes in place and returns the byte count.
  • Repr/Trace/nativeReprOwner gate inspecting or stringifying a raw file/dir object 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 dispatch through ordinary lookup — no send special case and no metatheory ripple. Only class methods that exist in CRuby are installed, so Dir.read-style typos still reach the prelude's method_missing and answer NoMethodError exactly as CRuby does. The prelude's File.basename/dirname/extname/join are unchanged (module File → class File to reopen the boot class).

Boot-shift repairs the new classes forced

  • intMetaId/strMetaId (prelude-booted heap ids) 79/88 → 87/96; #guard bootOkB catches a stale value. Deriving them from the heap is tracked as debt (see follow-up).
  • ConstantReachControls' concrete control heap grew one object; its Next constant now points at .ref 48.
  • runFS_frame + pathArg?/VFS.lookup framing lemmas join rootFrameLem; runModules_frame's terminal is now runFS.
  • bootGlobalConsts gains IO/Dir.

Verification (empirical)

  • lake build rubycore and the active-ratchet target: green.
  • #guard bootOkB: passes.
  • ./scripts/run_typed_ratchet.sh: RATCHET GREEN (validateD_safe_run passes for the enabled clinks).
  • ./scripts/check-proofs.sh: passes; every theorem rests on propext + Classical.choice + Quot.sound.
  • ./scripts/check-isolation.sh: Ratchet/ still does not see RubyCore/.
  • Model vs CRuby 4.0.5, byte-for-byte, on the step-1 surface: File.read/size/exist?/file?/directory? (fixture and missing path), Dir.exist?, File.write-then-read, File.basename, and ../. resolution (/tmp/vfsdata/../readme.txt). File.open (no block, step 2) and a missing path gate with named reasons.

Not in this PR (next steps, per #7 ship order)

Authored by Nori, an autonomous agent. Follow-up debt found while landing this is tracked in #22.

This was referenced Oct 4, 2026
Closed
Open
Open
Open
Open
Closed
Merged
Open
Closed
sam-xif pushed a commit that referenced this pull request Oct 10, 2026
@nori-agent
Derive the boot metaclass ids instead of pinning them (issue #22)
67a049f 
`intMetaId`/`strMetaId` are now `opaque` definitions read off the
prelude-booted heap, so adding a bootstrap class or boot-time eigenclass no
longer requires editing `State.lean` (PR #21 moved them 76/85 -> 87/96 by
hand). `opaque` keeps proofs from unfolding the prelude, which the kernel
cannot reduce. The values stay 76/85, so the corpus is unaffected, and a new
`#eval` names the offending id if the derivation lands on 0 or a non-class
object. `ConstantReachControls`'s scratch heap size is now `Boot.mainId + 3`
for the same reason.

Gate: `run_typed_ratchet.sh` GREEN, 125/125 clinks, 256 agree / 0 disagree,
131/263 corpus rungs, 46/46 negative controls.

Authored by Nori, an agent.
@nori-agent
VFS step 1: File.read/write/exist?/file?/directory?/size over a boot …
0238a79 
…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).
@nori-agent
VFS step 1: give directories a parent so .. resolves
1fc30e4 
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).
@sam-xif
sam-xif force-pushed the nori/vfs-step1-file-read-write branch from 2da15f8 to 1fc30e4 Compare October 10, 2026 04:04
sam-xif pushed a commit that referenced this pull request Oct 10, 2026
@nori-agent
Derive the boot metaclass ids instead of pinning them (issue #22)
57a187c 
`intMetaId`/`strMetaId` are now `opaque` definitions read off the
prelude-booted heap, so adding a bootstrap class or boot-time eigenclass no
longer requires editing `State.lean` (PR #21 moved them 76/85 -> 87/96 by
hand). `opaque` keeps proofs from unfolding the prelude, which the kernel
cannot reduce. The values stay 76/85, so the corpus is unaffected, and a new
`#eval` names the offending id if the derivation lands on 0 or a non-class
object. `ConstantReachControls`'s scratch heap size is now `Boot.mainId + 3`
for the same reason.

Gate: `run_typed_ratchet.sh` GREEN, 125/125 clinks, 256 agree / 0 disagree,
131/263 corpus rungs, 46/46 negative controls.

Authored by Nori, an agent.
This was referenced Oct 10, 2026
Open
Open
@sam-xif
sam-xif merged commit 5a1d7e8 into main Oct 10, 2026
4 checks passed
@sam-xif sam-xif mentioned this pull request Oct 10, 2026
Open
jiro-by-nori Bot added a commit that referenced this pull request Nov 6, 2026
@jiro-by-nori @nori-agent
Derive the boot metaclass ids instead of pinning them (issue #22)
ad3c48e 
`intMetaId`/`strMetaId` are now `opaque` definitions read off the
prelude-booted heap, so adding a bootstrap class or boot-time eigenclass no
longer requires editing `State.lean` (PR #21 moved them 76/85 -> 87/96 by
hand). `opaque` keeps proofs from unfolding the prelude, which the kernel
cannot reduce. The values stay 76/85, so the corpus is unaffected, and a new
`#eval` names the offending id if the derivation lands on 0 or a non-class
object. `ConstantReachControls`'s scratch heap size is now `Boot.mainId + 3`
for the same reason.

Gate: `run_typed_ratchet.sh` GREEN, 125/125 clinks, 256 agree / 0 disagree,
131/263 corpus rungs, 46/46 negative controls.

Authored by Nori, an agent.

Co-authored-by: Nori <contact@tilework.tech>
@jiro-approver-samxif jiro-approver-samxif Bot mentioned this pull request Nov 6, 2026
Open
jiro-by-nori Bot added a commit that referenced this pull request Nov 7, 2026
@jiro-by-nori @nori-agent
Size the constant-reach control heap at mainId + 1
dbf340b 
The control is a hand-built heap whose highest live index is the main
object at Boot.mainId. Sizing it at mainId + 3 grew the heap by two slots
and moved the fresh class' id to mainId + 3 (50), even though the literal
it replaces (48) is mainId + 1. Use mainId + 1 so the de-pinning keeps the
same heap and the same expected fresh id, and describe the present layout
rather than the pre-#21 one.

Addresses the review on #84.

Co-authored-by: Nori <contact@tilework.tech>
jiro-by-nori Bot added a commit that referenced this pull request Nov 8, 2026
@jiro-by-nori @nori-agent
Derive the boot metaclass ids instead of pinning them (issue #22)
ddfae35 
`intMetaId`/`strMetaId` are now `opaque` definitions read off the
prelude-booted heap, so adding a bootstrap class or boot-time eigenclass no
longer requires editing `State.lean` (PR #21 moved them 76/85 -> 87/96 by
hand). `opaque` keeps proofs from unfolding the prelude, which the kernel
cannot reduce. The values stay 76/85, so the corpus is unaffected, and a new
`#eval` names the offending id if the derivation lands on 0 or a non-class
object. `ConstantReachControls`'s scratch heap size is now `Boot.mainId + 3`
for the same reason.

Gate: `run_typed_ratchet.sh` GREEN, 125/125 clinks, 256 agree / 0 disagree,
131/263 corpus rungs, 46/46 negative controls.

Authored by Nori, an agent.

Co-authored-by: Nori <contact@tilework.tech>
jiro-by-nori Bot added a commit that referenced this pull request Nov 8, 2026
@jiro-by-nori @nori-agent
Size the constant-reach control heap at mainId + 1
754b86a 
The control is a hand-built heap whose highest live index is the main
object at Boot.mainId. Sizing it at mainId + 3 grew the heap by two slots
and moved the fresh class' id to mainId + 3 (50), even though the literal
it replaces (48) is mainId + 1. Use mainId + 1 so the de-pinning keeps the
same heap and the same expected fresh id, and describe the present layout
rather than the pre-#21 one.

Addresses the review on #84.

Co-authored-by: Nori <contact@tilework.tech>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@sam-xif @nori-agent