Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types

Summary

The best runtime check is the one that never runs. The problem The POSIX socket API is a state machine. A socket must be created, then bound, then set to listen, before it can accept connections. Calling operations in the wrong order — send on an unbound socket, accept before listen, close twice — is undefined behaviour in C. Every production socket library deals with this in one of three ways: Runtime checks — assert the state at every call, throw on violation (Python, Java, Go). Documentation — trust the programmer to read the man page (C, Rust). Ignore it — let the OS return EBADF and hope someone checks the return code. All three push the bug to runtime. Lean 4 offers a fourth option: make the bug unrepresentable at the type level, then erase the proof at compile time so the generated code is identical to raw C. The state machine Five states, seven transitions, and one proof obligation. That is the entire POSIX socket protocol. Let us encode it. Step 1: States as an inductive type inductive SocketState where | fresh -- socket() returned, nothing else happened | bound -- bind() succeeded | listening -- listen() succeeded | connected -- connect() or accept() produced this socket | closed -- close() succeeded — terminal state deriving DecidableEq DecidableEq gives us by decide for free — the compiler can prove any two concrete states are distinct without any user effort. Step 2: The socket carries its state as a phantom parameter structure Socket (state : SocketState) where protected mk :: raw : RawSocket -- opaque FFI handle (lean_alloc_external) The state parameter exists only at the type level. It is erased at runtime: a Socket .fresh and a Socket .connected have the exact same memory layout (a single pointer to the OS file descriptor). Zero overhead. The constructor is protected to prevent casual state fabrication. Step 3: Each function declares its pre- and post-state -- Creation: produces .fresh def socket (fam : Family) (typ : SocketType) : IO (Socket .fresh...