AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › arm64-semantics/Arm64/Trusted/Syscalls/Include › Errno.leanTier 3 · arm64-semantics

Errno.lean🔗

Tier 3 · arm64-semantics used by the symbolic proof 2 headline theorems depend on it 16 of 43 lines trusted source ↗

Trusted, reviewed with the engine. The AArch64 model in arm64-semantics is Tier 3: it is reviewed in its own repository (check-trust-guards). The declarations that the headline statements use are shown for completeness.

Declarations on this page (14)

Linux UAPI Error Numbers

Linux AArch64 errno constants from include/uapi/asm-generic/errno-base.h (EPERM = 1 .. ENOTTY = 25, EFAULT_RET = -14) and include/uapi/asm-generic/errno.h (ENAMETOOLONG = 36).

@[expose] public section
namespace Arm64

def EPERML25–26 ↗#

Linux EPERM (1, include/uapi/asm-generic/errno-base.h).

def EPERM : BitVec 64 := 1#64

def ENOENTL27 ↗#

def ENOENT : BitVec 64 := 2#64

def ESRCHL28 ↗#

def ESRCH : BitVec 64 := 3#64

def ENXIOL29 ↗#

def ENXIO : BitVec 64 := 6#64

def EBADFL30 ↗#

def EBADF : BitVec 64 := 9#64

def ENOMEML31 ↗#

def ENOMEM : BitVec 64 := 12#64

def EEXISTL32 ↗#

def EEXIST : BitVec 64 := 17#64

def ENOTDIRL33 ↗#

def ENOTDIR : BitVec 64 := 20#64

def EISDIRL34 ↗#

def EISDIR : BitVec 64 := 21#64

def EINVALL35 ↗#

def EINVAL : BitVec 64 := 22#64

def EMFILEL36 ↗#

def EMFILE : BitVec 64 := 24#64

def ENOTTYL37 ↗#

def ENOTTY : BitVec 64 := 25#64

def ENAMETOOLONGL38 ↗#

def ENAMETOOLONG : BitVec 64 := 36#64

def EFAULT_RETL40–41 ↗#

Linux -EFAULT error return (-14, include/uapi/asm-generic/errno-base.h:18).

def EFAULT_RET : BitVec 64 := -14#64
end Arm64