Canonical filesystem binding: actual FD identities/ownership, real DIR registry and race/borrow-aware raw output. Host resources/metadata remain leaves.

@[reducible, inline]

abbrev Miri.Interpreter.UnixFsMachine.Ref (H D O : Type) : Type

Equations

• Miri.Interpreter.UnixFsMachine.Ref H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

def Miri.Interpreter.UnixFsMachine.bindMetadata {K U H D O E HM P T : Type} (h : ReadinessMachine.Hooks K U H D O) (files : Files.Hooks (MachineHooks.State K U) H D O E HM) (otherMetadata : O → MachineHooks.M K U (Except (IoError.HostError E) HM ⊕ String)) (base : UnixFsMetadata.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E) : UnixFsMetadata.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E

Equations

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

def Miri.Interpreter.UnixFsMachine.insertDescription {K U H D O : Type} (h : ReadinessMachine.Hooks K U H D O) (description : Files.Description H D O) : MachineHooks.M K U (Int32 × Files.FdId)

Entire actual owned handle insertion, with stable source descriptor identity.

Equations

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

structure Miri.Interpreter.UnixFsMachine.DirectoryStore (U R : Type) : Type

• get : U → UnixDirectories.Table R
• put : UnixDirectories.Table R → U → U

def Miri.Interpreter.UnixFsMachine.bindDirectories {K U H D O R E HM P T Kind Ent : Type} (h : ReadinessMachine.Hooks K U H D O) (store : DirectoryStore U R) (readiness : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) (fd : UnixFd.Hooks (MachineHooks.State K U) H D O E HM) (base : UnixDirectories.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind R Ent) : UnixDirectories.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind R Ent

Equations

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

def Miri.Interpreter.UnixFsMachine.bindFd {K U H D O E HM P T Kind : Type} (_h : ReadinessMachine.Hooks K U H D O) (files : Files.Hooks (MachineHooks.State K U) H D O E HM) (base : UnixFsFd.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H) : UnixFsFd.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H

Equations

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

def Miri.Interpreter.UnixFsMachine.bindTemporary {K U H D O P HM T E Kind : Type} (h : ReadinessMachine.Hooks K U H D O) (base : UnixTempFile.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H) : UnixTempFile.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H

Equations

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

def Miri.Interpreter.UnixFsMachine.bindFlock {S H E D O : Type} (host : UnixFileOperations.Hooks S H E) (asUnix : Ref H D O → EStateM StepError S Unit) (other : O → Bool → UnixFileOperations.LockOp → EStateM StepError S (Except (IoError.HostError E) Unit)) (ref : Ref H D O) (communicate : Bool) (operation : UnixFileOperations.LockOp) : EStateM StepError S (Except (IoError.HostError E) Unit)

FileDescription downcast preserves unsupported default flock on other kinds.

Equations

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

def Miri.Interpreter.UnixFsMachine.bindAll {K U H D O E HM R P T Kind Ent : Type} (h : ReadinessMachine.Hooks K U H D O) (files : Files.Hooks (MachineHooks.State K U) H D O E HM) (otherMetadata : O → MachineHooks.M K U (Except (IoError.HostError E) HM ⊕ String)) (store : DirectoryStore U R) (readiness : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) (fd : UnixFd.Hooks (MachineHooks.State K U) H D O E HM) (base : UnixFsDispatch.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H R Ent) : UnixFsDispatch.Hooks (MachineHooks.State K U) (Ref H D O) D P HM T E Kind H R Ent

Share one canonical metadata/path/FD adapter through every filesystem arm.

Equations

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

def Miri.Interpreter.UnixFsMachine.bindRawWrites {K U F D P HM T E Kind : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K U) (arithmetic : Memory.PointerArithmetic) (base : UnixFsPaths.Hooks (MachineHooks.State K U) F D P HM T E Kind) : UnixFsPaths.Hooks (MachineHooks.State K U) F D P HM T E Kind

Reuses actual allocation access (race then borrow checks), initialization and provenance-clearing writes for readlink and generated directory names.

Equations

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

def Miri.Interpreter.UnixFsMachine.bindTimes {S Host T Zone Stamp F D P HM E Kind H : Type} (time : TimeShims.Hooks S Host T Zone Stamp) (base : UnixFsTimes.Hooks S F D P HM T E Kind H) : UnixFsTimes.Hooks S F D P HM T E Kind H

Actual time reader and SystemTime clock; host checked UNIX_EPOCH arithmetic and set_times remain the typed filesystem host boundary.

Equations

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

def Miri.Interpreter.UnixFsMachine.directoryRoots {R : Type} (table : UnixDirectories.Table R) : Array (Memory.Pointer (Option Memory.Provenance))

Source DirTable::visit_provenance visits exactly each last-returned entry.

Equations

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