FileIo.lean🔗

File-System and File-Descriptor Syscalls

Re-exports Arm64.Trusted.Syscalls.Fs.{ReadWrite,Open,Stat,Fcntl,Ioctl} and bundles their handlers with Stdio into Syscall.fileIoOnlyTable, Syscall.fileIoTable, and Syscall.fileIo.

@[expose] public section

namespace Arm64

namespace Syscall

def fileIoOnlyTableL33–41 ↗#

Dispatch entries specific to file-descriptor and path operations (excluding Stdio).

def fileIoOnlyTable : List (BitVec 64 × (State → State)) :=
  [(SYS_FCNTL, execFcntl),
   (SYS_IOCTL, execIoctl),
   (SYS_OPENAT, execOpenat),
   (SYS_CLOSE, execClose),
   (SYS_LSEEK, execLseek),
   (SYS_PREAD64, execPread64),
   (SYS_FSTAT, execFstat)]

2 declarations not shown (lines 43–49): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.fileIoTable, Arm64.Syscall.fileIo

end Syscall

end Arm64