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

books/Books/FastPower/Proof.lean

@@ -74,17 +74,17 @@ def entry (b n : Int) : Machine := (stepN 61 (start (program b n))).getD default
 /-- The machine at the loop test when the loop's variables hold these values.
     Everything the loop does not touch is taken from `entry`; what it does
     touch is spelled out — the locals of `raise_to`'s frame (frame 3) and the
-    instance variables of the `Power` object (object 105), whose `revision`
+    instance variables of the `Power` object (object 114), whose `revision`
     counts the writes it has received. -/
 def loopHead (b n : Int) (result square left : Int) (steps : Nat) : Machine :=
   let m := entry b n
   let f := m.frames.getD 3 default
-  let o := m.heap.objs.getD 105 default
+  let o := m.heap.objs.getD 114 default
   { m with
     frames := m.frames.set! 3 { f with locals :=
       [("left", .int left), ("square", .int square), ("result", .int result),
        ("exponent", .int n)] }
-    heap := { m.heap with objs := m.heap.objs.set! 105 { o with
+    heap := { m.heap with objs := m.heap.objs.set! 114 { o with
       ivars := [("@steps", .int steps), ("@base", .int b)], revision := steps + 2 } } }
 
 /-- `left > 0` has been evaluated to `t` and the `while` is about to act on it. -/
@@ -151,7 +151,7 @@ theorem finish (b n r s e : Int) (c : Nat) :
     stepFn (final b n r s e c) = .done (outcome b n r s e c).1 (outcome b n r s e c).2 := by
   kernel_rfl
 
-theorem outcome_value (b n r s e : Int) (c : Nat) : (outcome b n r s e c).1 = .ref 106 := by
+theorem outcome_value (b n r s e : Int) (c : Nat) : (outcome b n r s e c).1 = .ref 115 := by
   kernel_rfl
 
 /-- What `puts answer` wrote: the decimal digits of `result` and a newline. -/
@@ -161,7 +161,7 @@ theorem outcome_out (b n r s e : Int) (c : Nat) :
 
 /-- The value is an Array of the final `result` and `@steps`. -/
 theorem outcome_array (b n r s e : Int) (c : Nat) :
-    ((outcome b n r s e c).2.heap.get 106).payload = .arr #[.int r, .int c] := by kernel_rfl
+    ((outcome b n r s e c).2.heap.get 115).payload = .arr #[.int r, .int c] := by kernel_rfl
 
 /-! ## 3. Arithmetic -/
 
@@ -291,7 +291,7 @@ theorem fast_power_correct (b n : Int) :
   let r := b ^ n.toNat
   let c := bitLength n.toNat
   refine ⟨(outcome b n r s' e' c).1, (outcome b n r s' e' c).2, ⟨_, boot_ok _, ?_⟩, ?_,
-    106, outcome_value b n r s' e' c, outcome_array b n r s' e' c⟩
+    115, outcome_value b n r s' e' c, outcome_array b n r s' e' c⟩
   · exact .of_reaches
       ((Reaches.of_stepN (setup b n)).trans <| hloop.trans (.of_stepN (leave b n r s' e' c)))
       (finish b n r s' e' c)

books/Books/Metatheory/Framing/RootFramePrimitives.lean

@@ -849,6 +849,34 @@ set_option maxRecDepth 400000 in
     | split)
   all_goals root_hof
 
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 400000 in
+@[rootFrameLem] theorem pathArg?_frame (K : List Kont) (m : Machine) (v : Value) :
+    Builtins.pathArg? (pushRootK K m) v = Builtins.pathArg? m v := by
+  cases v <;> simp [Builtins.pathArg?, pushRootK_heap]
+
+@[rootFrameLem] theorem vfs_lookup_frame (K : List Kont) (m : Machine) (p : String) :
+    VFS.lookup (pushRootK K m).heap p = VFS.lookup m.heap p := by
+  simp [VFS.lookup, VFS.resolve, pushRootK_heap]
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 400000 in
+@[rootFrameLem] theorem runFS_frame (K : List Kont) (bid : String) (recv : Value)
+    (args : List Value) (m : Machine) :
+    runFS bid recv args (pushRootK K m) = bRootPush K (runFS bid recv args m) := by
+  rw [runFS.eq_def, runFS.eq_def]
+  root_simp
+  root_arms
+  all_goals root_hof
+  all_goals (repeat' first
+    | rfl
+    | (simp only [rootFrameLem]; done)
+    | (simp [rootFrameLem]; done)
+    | (rw [foldPair_frame K]; try simp only [rootFrameLem])
+    | (rw [foldPairArray_frame K]; try simp only [rootFrameLem])
+    | intro _
+    | split)
+
 @[rootFrameLem] theorem nativeModuleName_frame (K : List Kont) (m : Machine) (cp : ClassPayload) :
     nativeModuleName (pushRootK K m) cp = bRootPush K (nativeModuleName m cp) := by
   unfold nativeModuleName

books/Books/TypeSoundness/Checker/Guards/GlobalConsts.lean

@@ -3,7 +3,7 @@ The semantic boot gate checks this data against the actual prelude heap. -/
 namespace Checker
 
 def bootGlobalConsts : List String :=
-  ["T", "Struct", "Encoding", "File", "URI", "Pathname", "JSON", "Forwardable",
+  ["T", "Struct", "Encoding", "File", "IO", "Dir", "URI", "Pathname", "JSON", "Forwardable",
    "Enumerable", "Comparable", "BasicObject", "Object", "Module", "Class", "NilClass",
    "TrueClass", "FalseClass", "Integer", "Float", "String", "Symbol", "Array", "Hash",
    "Exception", "StandardError", "RuntimeError", "ArgumentError", "TypeError", "NameError",

books/Books/TypeSoundness/Conformance/Core/State.lean

@@ -498,9 +498,16 @@ def coreClsNames : List String :=
    "IOError", "FrozenError", "NotImplementedError"]
 
 /-- The boot metaclasses of Integer and String: `Integer === x` and `String === x` dispatch
-from here, where Module#=== is installed (checked at boot by `coreDataB`). -/
-def intMetaId : ObjId := 76
-def strMetaId : ObjId := 85
+from here, where Module#=== is installed (checked at boot by `coreDataB`).
+
+These are ids in the **prelude-booted** heap (`Prelude.boot`), not `H₀`'s: phase 1
+realizes the `File`/`Dir`/`IO` singleton eigenclasses (issue #7 step 1) and the
+exception eigenclasses, so the ids depend on the whole boot. They are re-pinned by
+hand whenever a bootstrap class or a boot-time eigenclass is added, and `#guard
+bootOkB` catches a stale value. Deriving them from the heap instead of pinning
+them is tracked as follow-up debt. -/
+def intMetaId : ObjId := 87
+def strMetaId : ObjId := 96
 
 /-- **The core classes are what they are.**
 

books/Books/TypeSoundness/Controls/ConstantReachControls.lean

@@ -22,7 +22,7 @@ private def eigenPayload : ClassPayload :=
   { superclass := some Boot.basicObjectId, name := "", attached := some 45, methods := hooks }
 private def eigenObj : Object := { klass := Boot.classId, payload := .cls eigenPayload }
 private def h : Heap :=
-  { objs := ((((Array.replicate 47 (default : Object)).set! 0 basic).set! 1 root).set! 45 detached).set! 46 eigenObj }
+  { objs := ((((Array.replicate 48 (default : Object)).set! 0 basic).set! 1 root).set! 45 detached).set! 46 eigenObj }
 private def m : Machine :=
   { ctl := .value .nil, heap := h,
     frames := #[{ self := .ref Boot.mainId, defmod := Boot.objectId, cref := [], kind := .toplevel }], stack := [0] }
@@ -86,7 +86,7 @@ theorem old_site_not_preserved :
   intro site
   have he := site.constants "Next"
   have hmiss : instanceConstResolve (FreshClassActual.heap m "Next" 46) 45 "Next" = none := rfl
-  have hglobal : constLookup (FreshClassActual.heap m "Next" 46) "Next" = some (.ref 47) := rfl
+  have hglobal : constLookup (FreshClassActual.heap m "Next" 46) "Next" = some (.ref 48) := rfl
   rw [hmiss, hglobal] at he
   cases he
 

ruby-lean/RubyCore/Boot.lean

@@ -46,6 +46,25 @@ def boot : Except String Machine :=
     let initial := Boot.classTable.foldl (fun m entry =>
       if (ancestors m.heap entry.1).contains Boot.exceptionId then
         (Interp.eigenclassOf m entry.1).2 else m) initial
+    -- Filesystem singleton methods (issue #7 step 1): the `File.`/`Dir.`/`IO.`
+    -- class methods that actually exist in CRuby and are modeled, installed on
+    -- the constants' eigenclasses here exactly like `Exception.exception`, and
+    -- reached by ordinary dispatch — no interpreter special case, and the
+    -- prelude's own `File.basename`/`method_missing` continue to resolve as
+    -- before. Only real CRuby class methods are installed, so an unknown call
+    -- still reaches the prelude's `method_missing` and gates rather than
+    -- answering.
+    let fsSingleton : List (ObjId × List String) :=
+      [ (Boot.fileId, ["read", "write", "exist?", "file?", "directory?", "size"]),
+        (Boot.dirId, ["exist?"]),
+        (Boot.ioId, ["read", "write"]) ]
+    let initial := fsSingleton.foldl (fun m (cls, names) =>
+      let (eigen, m) := Interp.eigenclassOf m cls
+      let cname := match m.heap.classPayload? cls with | some c => c.name | none => ""
+      names.foldl (fun m name =>
+        let bid := cname ++ "#" ++ name
+        let md : MethodDef := { params := [], body := .nil, owner := eigen, builtin := some bid }
+        { m with heap := defineMethod m.heap eigen name md }) m) initial
     match Interp.run bootFuel initial with
     | .value _ m => .ok m
     | .uncaught exc m =>

ruby-lean/RubyCore/Builtins/FS.lean

@@ -0,0 +1,101 @@
+import RubyCore.Builtins.Regex
+
+/-!
+The filesystem singleton methods of issue #7 step 1: `File.read`/`write`/
+`exist?`/`file?`/`directory?`/`size` over the symbolic boot fixture
+(`RubyCore/Heap.lean` §Virtual filesystem).
+
+The pure machine never performs OS effects; every operation here reads or mutates
+the fixture tree that lives in the heap. An unmodeled operation is a named
+`Unsupported` — never a guessed value and never a fake `Errno` (issue #7's
+"gate stays honest"). `Errno` classes and message fidelity are step 7.
+
+`File.write` mutates inode bytes in place; `flush` is a no-op because descriptor
+writes update the inode on write (the documented step-2 simplification, and the
+only descriptor behavior step 1 needs).
+-/
+
+namespace RubyCore
+
+namespace Builtins
+
+/-- Read a String argument as a path, or `none` if it is not a String. -/
+def pathArg? (m : Machine) : Value → Option String
+  | .ref o => match (m.heap.get o).payload with
+    | .str s => some s
+    | _ => none
+  | _ => none
+
+/-- A `File.*` / `Dir.*` / `IO.*` singleton operation. `recv` is the class
+    object; `args` are the Ruby arguments. -/
+def runFS (bid : String) (recv : Value) (args : List Value) (m : Machine) : BRes :=
+  let h := m.heap
+  match bid with
+  | "File#read" | "IO#read" =>
+    match args with
+    | [p] =>
+      match pathArg? m p with
+      | some path =>
+        match VFS.lookup h path with
+        | some o =>
+          match (h.get o).payload with
+          | .file bytes => okStr m bytes
+          | .dir _ _ => .unsupported "File.read: is a directory (Errno::EISDIR gated at step 1)"
+          | _ => .unsupported "File.read: not a regular file"
+        | none => .unsupported "File.read: no such file (Errno::ENOENT gated at step 1)"
+      | none => .unsupported "File.read: path argument is not a String"
+    | _ => .unsupported s!"{bid}: argument shape outside step 1"
+  | "File#write" | "IO#write" =>
+    match args with
+    | [p, data] =>
+      match pathArg? m p, pathArg? m data with
+      | some path, some bytes =>
+        match VFS.lookup h path with
+        | some o =>
+          match (h.get o).payload with
+          | .file _ =>
+            let h' := h.set o { h.get o with payload := .file bytes }
+            .ok (.int (Int.ofNat bytes.length)) { m with heap := h' }
+          | .dir _ _ => .unsupported "File.write: is a directory (Errno::EISDIR gated at step 1)"
+          | _ => .unsupported "File.write: not a regular file"
+        | none => .unsupported "File.write: no such file (Errno::ENOENT gated at step 1)"
+      | _, _ => .unsupported "File.write: path or data argument is not a String"
+    | _ => .unsupported s!"{bid}: argument shape outside step 1"
+  | "File#exist?" | "Dir#exist?" =>
+    match args with
+    | [p] => (match pathArg? m p with
+      | some path => .ok (.bool (VFS.lookup h path).isSome) m
+      | none => .unsupported s!"{bid}: path argument is not a String")
+    | _ => .unsupported s!"{bid}: argument shape outside step 1"
+  | "File#file?" =>
+    match args with
+    | [p] => (match pathArg? m p with
+      | some path => match VFS.lookup h path with
+        | some o => .ok (.bool (match (h.get o).payload with | .file _ => true | _ => false)) m
+        | none => .ok (.bool false) m
+      | none => .unsupported s!"{bid}: path argument is not a String")
+    | _ => .unsupported s!"{bid}: argument shape outside step 1"
+  | "File#directory?" =>
+    match args with
+    | [p] => (match pathArg? m p with
+      | some path => match VFS.lookup h path with
+        | some o => .ok (.bool (match (h.get o).payload with | .dir _ _ => true | _ => false)) m
+        | none => .ok (.bool false) m
+      | none => .unsupported s!"{bid}: path argument is not a String")
+    | _ => .unsupported s!"{bid}: argument shape outside step 1"
+  | "File#size" =>
+    match args with
+    | [p] => (match pathArg? m p with
+      | some path => match VFS.lookup h path with
+        | some o => match (h.get o).payload with
+          | .file bytes => .ok (.int (Int.ofNat bytes.length)) m
+          | .dir _ _ => .unsupported "File.size: is a directory (Errno::EISDIR gated at step 1)"
+          | _ => .unsupported "File.size: not a regular file"
+        | none => .unsupported "File.size: no such file (Errno::ENOENT gated at step 1)"
+      | none => .unsupported "File.size: path argument is not a String")
+    | _ => .unsupported "File#size: argument shape outside step 1"
+  | _ => runRegex bid recv args m
+
+end Builtins
+
+end RubyCore

ruby-lean/RubyCore/Builtins/Modules.lean

@@ -1,4 +1,5 @@
 import RubyCore.Builtins.Regex
+import RubyCore.Builtins.FS
 import RubyCore.Generated.CRubyNames
 
 /-!
@@ -253,7 +254,7 @@ def runModules (bid : String) (recv : Value) (args : List Value) (m : Machine) :
         if names.length != args.length then .unsupported "constant visibility: name conversion" else
         setConstantVisibility m recv o (bid == "Module#private_constant") names
     | _ => .unsupported "private_constant on a non-module"
-  | _ => runRegex bid recv args m
+  | _ => runFS bid recv args m
 
 end Builtins
 

ruby-lean/RubyCore/Builtins/Support.lean

@@ -110,6 +110,8 @@ def nativeReprOwner (h : Heap) (name : String) : Value → String
     | .mdata .. => "MatchData"
     | .enumerator _ => if name == "to_s" then "Object" else "Enumerator"
     | .chain _ => if name == "to_s" then "Object" else "Enumerator::Chain"
+    | .file _ => "File"
+    | .dir _ _ => "Dir"
 
 def reprUnchanged (h : Heap) (sens : List String) (value : Value) : Bool :=
   sens.all fun name =>

ruby-lean/RubyCore/Generated/Prelude.lean

@@ -8793,8 +8793,9 @@ def core_46 : Expr :=
            none))))
 
 def core_47 : Expr :=
-  RubyCore.Expr.module'
+  RubyCore.Expr.class'
     "File"
+    none
     (RubyCore.Expr.seq
       [RubyCore.Expr.casgn "SEPARATOR" (RubyCore.Expr.str "/"),
        RubyCore.Expr.defs