Source construction for the pinned Unix filesystem shim family. Compiler ABI facts, guest memory, descriptors and directory storage stay in the actual EvalWorld. This layer accepts only raw host filesystem effects; policy remains in the existing UnixFs interpreter modules.

@[reducible, inline]

abbrev Miri.Input.EvalUnixFsConstruction.M (σ α : Type) : Type

Equations

• Miri.Input.EvalUnixFsConstruction.M = EStateM Miri.Interpreter.StepError

structure Miri.Input.EvalUnixFsConstruction.HostEffects (S H D O Path HM Time E ReadDir Entry : Type) : Type

Actual host operations not represented by the current source seed. Values are raw std::fs/path/ReadDir observations; this record has no guest-memory, compiler-layout, errno, descriptor-table, directory-table or shim-policy callbacks.

• hostUnix : Bool
• hostWindows : Bool
• hostUsizeBits : Nat

  Width of this host's usize, used by source host-boundary checks.

• isEmpty : Path → Bool
• isAbsolute : Path → Bool
• isDot : Path → Bool
• emptyPath : Path
• procAbsolute : Path → M S Bool

  Exact path::absolute(path).is_ok_and(|p| p.starts_with("/proc")).

• currentExe : M S (Option Path)
• pathToString : Path → Option String
• removeFile : Path → M S (Except (Interpreter.IoError.HostError E) Unit)
• removeDirectory : Path → M S (Except (Interpreter.IoError.HostError E) Unit)
• symlinkDirectory : Path → M S Bool
• linkTargetDirectory : Path → Path → M S Bool
• createSymlink : Path → Path → Bool → M S (Except (Interpreter.IoError.HostError E) Unit)
• hardLink : Path → Path → M S (Except (Interpreter.IoError.HostError E) Unit)
• setPathPermissions : Path → UInt32 → M S (Except (Interpreter.IoError.HostError E) Unit)
• rename : Path → Path → M S (Except (Interpreter.IoError.HostError E) Unit)
• mkdir : Path → Option UInt32 → M S (Except (Interpreter.IoError.HostError E) Unit)
• readLink : Path → M S (Except (Interpreter.IoError.HostError E) Path)
• canonicalize : Path → M S (Except (Interpreter.IoError.HostError E) Path)
• pathMetadata : Option D → Path → Bool → M S (Except (Interpreter.IoError.HostError E) HM)
• fileType : HM → Interpreter.UnixFsMetadata.FileType
• length : HM → UInt64
• time : HM → Interpreter.UnixFsMetadata.TimeField → M S (Except (Interpreter.IoError.HostError E) Time)
• sinceEpoch : Time → M S Interpreter.Clock.Duration
• unixFields : HM → Interpreter.UnixFsMetadata.UnixFields
• readonly : HM → Bool
• readDir : Path → M S (Except (Interpreter.IoError.HostError E) ReadDir)
• openDirectory : Path → M S (Except (Interpreter.IoError.HostError E) D)
• dropReadDir : ReadDir → M S Unit
• nextEntry : ReadDir → M S (Option (Except (Interpreter.IoError.HostError E) Entry))
• entryName : Entry → Path
• entryType : Entry → M S (Except (Interpreter.IoError.HostError E) Interpreter.UnixFsMetadata.FileType)
• entryInode : Entry → UInt64
• setLength : H → UInt64 → M S (Except (Interpreter.IoError.HostError E) Unit)
• fileLength : H → M S (Except (Interpreter.IoError.HostError E) UInt64)
• setFilePermissions : H → UInt32 → M S (Except (Interpreter.IoError.HostError E) Unit)
• sync : H → Bool → M S (Except (Interpreter.IoError.HostError E) Unit)
• isTty : Interpreter.Files.Ref (Interpreter.Files.Description H D O) → Bool → M S Bool
• systemNow : M S Time
• sinceEpochCheckedAdd : Interpreter.Clock.Duration → M S (Option Time)
• setFileTimes : H → Interpreter.UnixFsTimes.Update Time → Interpreter.UnixFsTimes.Update Time → M S (Except (Interpreter.IoError.HostError E) Unit)
• setPathTimes : Path → Bool → Interpreter.UnixFsTimes.Update Time → Interpreter.UnixFsTimes.Update Time → M S (Except (Interpreter.IoError.HostError E) Unit)
• openExclusive : Path → Interpreter.UnixTempFile.HostOptions → M S (Except (Interpreter.IoError.HostError E) H)

def Miri.Input.EvalUnixFsConstruction.metadataFromSource {U C Os Kind Path E H D O HM Time ReadDir Entry : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind U) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) C Interpreter.MachineHooks.FrameExtra) (choice : C) (strings : Interpreter.OsStrings.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) Os Kind) (pathFromOs : Os → Path) (errors : Interpreter.IoError.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) E) (registry : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U) H D O) (files : Interpreter.Files.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O E HM) (otherMetadata : O → M (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Except (Interpreter.IoError.HostError E) HM ⊕ String)) (host : HostEffects (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O Path HM Time E ReadDir Entry) (os : String) (isolatedOp : EvalUnixConstruction.IsolatedOp) : Except Interpreter.StepError (Interpreter.UnixFsMetadata.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E)

Canonical stat metadata access, including compiler-owned exact named layouts/constants and FD lookups from the existing source descriptor table.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.osStringsFromSource {Os U C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (host : EvalHostRuntimeConstruction.OsHostEffects Os) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control U) C Payload) : Interpreter.OsStrings.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) Os (Memory.MemoryKind Memory.MiriMemoryKind)

Build the path string codec over the same EvalWorld memory, but expose the actual allocator kind: realpath(NULL) calls Miri's C allocator, while the ordinary environment-string builder only exposes its narrower env kinds.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.osStringsFromSource.scan {U : Type} [DecidableEq Memory.MiriMemoryKind] (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User (Interpreter.ValidityMachine.Control U))) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control U)) (base : Memory.Pointer (Option Memory.Provenance)) (fuel length : Nat) : M (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) UInt64

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalUnixFsConstruction.osStringsFromSource.scan access pointer base 0 length = throw (Miri.Interpreter.StepError.resourceExhaustion "C string scan budget")

def Miri.Input.EvalUnixFsConstruction.pathsFromSource {U C Payload F D Path HM Time E Os H O ReadDir Entry : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind U) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control U) C Payload) (metadata : Interpreter.UnixFsMetadata.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) F D Path HM Time E) (strings : Interpreter.OsStrings.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) Os (Memory.MemoryKind Memory.MiriMemoryKind)) (pathFromOs : Os → Path) (osFromPath : Path → Os) (host : HostEffects (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O Path HM Time E ReadDir Entry) : Except Interpreter.StepError (Interpreter.UnixFsPaths.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) F D Path HM Time E (Memory.MemoryKind Memory.MiriMemoryKind))

Canonical pathname shim hooks. All ABI reads/writes use the existing guest access and compiler layouts; the only supplied values are actual raw host path operations and the same source OS-string representation.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.fdFromSource {S H D O Path HM Time E Kind ReadDir Entry : Type} (paths : Interpreter.UnixFsPaths.Hooks S (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E Kind) (files : Interpreter.Files.Hooks S H D O E HM) (communicate : Bool) (host : HostEffects S H D O Path HM Time E ReadDir Entry) : Interpreter.UnixFsFd.Hooks S (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E Kind H

Bind file-only filesystem operations to the canonical Files implementation and the same owned descriptor references used by readiness and close.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.timesFromSource {U C Payload H D O Path HM Time E ReadDir Entry : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind U) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) C Interpreter.MachineHooks.FrameExtra) (choice : C) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control U) C Payload) (fd : Interpreter.UnixFsFd.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E (Memory.MemoryKind Memory.MiriMemoryKind) H) (host : HostEffects (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O Path HM Time E ReadDir Entry) : Interpreter.UnixFsTimes.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E (Memory.MemoryKind Memory.MiriMemoryKind) H

Source timespec input and host file-time operations. Field identities and layouts come from the selected compiler; reads still pass through the active borrow/race/initialization access engine.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.directoriesFromSource {U C Payload H D O Path HM Time E ReadDir Entry : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) C Interpreter.MachineHooks.FrameExtra) (choice : C) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control U) C Payload) (paths : Interpreter.UnixFsPaths.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E (Memory.MemoryKind Memory.MiriMemoryKind)) (registry : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U) H D O) (readiness : Interpreter.Readiness.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O))) (fd : Interpreter.UnixFd.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O E HM) (store : Interpreter.UnixFsMachine.DirectoryStore (Interpreter.ValidityMachine.UserState U) ReadDir) (host : HostEffects (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) H D O Path HM Time E ReadDir Entry) : Interpreter.UnixDirectories.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState U)) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E (Memory.MemoryKind Memory.MiriMemoryKind) ReadDir Entry

Reuse the one rooted runtime DIR table and allocate/write dirent results through compiler-provided layouts and the active source memory access.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalUnixFsConstruction.temporaryFromSource {U H D O Path HM Time E Kind ReadDir Entry : Type} (paths : Interpreter.UnixFsPaths.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind U) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E Kind) (registry : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind U H D O) (choose : Nat → Interpreter.MachineHooks.M Memory.MiriMemoryKind U Nat) (host : HostEffects (Interpreter.MachineHooks.State Memory.MiriMemoryKind U) H D O Path HM Time E ReadDir Entry) (attemptBudget : Nat) : Interpreter.UnixTempFile.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind U) (Interpreter.Files.Ref (Interpreter.Files.Description H D O)) D Path HM Time E Kind H

Source mkstemp hooks over the actual RNG selection and owned FD registry. The random action is passed separately from host FS leaves because its state is the interpreter's machine choice tape, not host nondeterminism.

Equations

• One or more equations did not get rendered due to their size.