Syscalls.lean🔗

Linux AArch64 Syscall Families Umbrella (Arm64.Trusted.Syscalls)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: Re-exports the modular Linux AArch64 syscall families under Arm64/Trusted/Syscalls/ (Common, Stdio, FileIo, Poll, Alloc, Signals, Time, Random, Misc) and defines the empty bundle Syscall.none, the full 31-entry dispatch table Syscall.standardTable, Syscall.standard, and the compatibility alias execSyscall.
When to read: Read Arm64/Trusted/Syscalls/README.md to pick the minimal bundle for a specification (noSyscalls, Syscall.stdioCli, Syscall.fileIo, ...) so unused syscall families stay outside the theorem statement's transitive constant closure.

@[expose] public section

namespace Arm64

namespace Syscall

1 declaration not shown (lines 41–42): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.none

def standardTableL44–46 ↗#

Complete 31-syscall Linux AArch64 dispatch table combining all modeled families.

def standardTable : List (BitVec 64 × (State → State)) :=
  stdioTable ++ fileIoOnlyTable ++ pollTable ++ allocTable ++ signalsTable ++ timeTable ++ randomTable ++ miscTable

def standardL48–50 ↗#

Full modeled Linux AArch64 syscall bundle (31 syscalls across Stdio, FileIo, Poll, Alloc, Signals, Time, Random, and Misc).

def standard : State → State := dispatch standardTable

end Syscall

1 declaration not shown (lines 54–58): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.execSyscall

end Arm64