Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean 4's Type System | NGrislain

NGrislain

About

Blog

Projects

Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean 4's Type System

March 25, 2026

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)

-- Binding: requires .fresh, produces .bound
def bind (s : Socket .fresh) (addr : SockAddr) : IO (Socket .bound)

-- Listening: requires .bound, produces .listening
def listen (s : Socket .bound) (backlog : Nat) : IO (Socket .listening)

-- Accepting: requires .listening, produces .connected
def accept (s : Socket .listening) : IO (Socket .connected × SockAddr)

-- Connecting: requires .fresh, produces .connected
def connect (s : Socket .fresh) (addr : SockAddr) : IO (Socket .connected)

-- Sending/receiving: requires .connected
def send (s : Socket .connected) (data : ByteArray) : IO Nat
def recv (s : Socket .connected) (maxlen : Nat) : IO ByteArray

The Lean 4 kernel threads these constraints through the program. If you write send freshSocket data, the kernel sees Socket .fresh where it expects Socket .connected, and reports a type error. No runtime check. No assertion. No exception. No branch in the generated code.

Step 4: Double-close prevention via proof obligation
def close (s : Socket state)
(_h : state ≠ .closed := by decide)
: IO (Socket .closed)

This is where dependent types shine brightest. The second parameter is a proof that the socket is not already closed. Let us trace what happens for each concrete state:
CallProof obligationby decideResultclose (s : Socket .fresh).fresh ≠ .closedtrivially truecompilesclose (s : Socket .bound).bound ≠ .closedtrivially truecompilesclose (s : Socket .listening).listening ≠ .closedtrivially truecompilesclose (s : Socket .connected).connected ≠ .closedtrivially truecompilesclose (s : Socket .closed).closed ≠ .closedimpossibletype error
For the first four, the default tactic by decide discharges the proof automatically — the caller writes nothing. For the fifth, the proposition .closed ≠ .closed is logically false: no proof can exist, so the program is rejected at compile time.

The proof is erased during compilation. The generated C code is:
lean_object* close(lean_object* socket) {
close_fd(lean_get_external_data(socket));
return lean_io_result_mk_ok(lean_box(0));
}

No branch. No flag. No state field. The proof did its job during type-checking and vanished.

Step 5: Distinctness theorems

We also prove that all five states are pairwise distinct:
theorem SocketState.fresh_ne_bound : .fresh ≠ .bound := by decide
theorem SocketState.fresh_ne_listening : .fresh ≠ .listening := by decide
theorem SocketState.fresh_ne_connected : .fresh ≠ .connected := by decide
theorem SocketState.fresh_ne_closed : .fresh ≠ .closed := by decide
theorem SocketState.bound_ne_listening : .bound ≠ .listening := by decide
-- ... (11 theorems total)

These are trivially proved by decide (the kernel evaluates the BEq instance). They exist so that downstream code can use them as lemmas without re-proving distinctness.

What the compiler actually rejects
-- ❌ send on a fresh socket
let s ← socket .inet .stream
send s "hello".toUTF8
-- Error: type mismatch — expected Socket .connected, got Socket .fresh

-- ❌ accept before listen
let s ← socket .inet .stream
let s ← bind s addr
accept s
-- Error: type mismatch — expected Socket .listening, got Socket .bound

-- ❌ double close
let s ← socket .inet .stream
let s ← close s
close s
-- Error: state ≠ .closed — proposition .closed ≠ .closed is false

-- ✅ correct sequence
let s ← socket .inet .stream
let s ← bind s ⟨"0.0.0.0", 8080⟩
let s ← listen s 128
let (conn, addr) ← accept s
let _ ← send conn "HTTP/1.1 200 OK\r\n\r\n".toUTF8
let _ ← close conn
let _ ← close s

Try it yourself

Open this example in the Lean 4 Playground — try uncommenting the failing examples to see the type errors live.

Uncomment bad_double_close or bad_send_fresh and the kernel rejects the program immediately — the error messages tell you exactly which state transition is invalid.

The punchline
ApproachLines of state-checking codeRuntime costCatches atC (man page)00never (UB)Python (runtime)~50branch per callruntimeRust (typestate)~300compile-timeLean 4 (dependent types)00compile-time
Lean 4 is unique: the proof obligation state ≠ .closed is a real logical proposition that the kernel verifies. It is not a lint, not a static analysis heuristic, not a convention. It is a mathematical proof of protocol compliance, checked by the same kernel that verifies Mathlib's theorems — and then thrown away so the generated code runs at the speed of C.

---

This post is part of the Hale documentation — a port of Haskell's web ecosystem to Lean 4 with maximalist typing.

This site is generated by Verso.

Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean 4’s Type System by NGridlain

This document details an innovative approach to implementing POSIX socket compliance in Lean 4, achieving “zero-cost” correctness through the integration of dependent types. The core problem addressed is the inherent complexity and potential for errors within the POSIX socket API, which mandates a specific sequence of operations—binding, listening, connecting, accepting, and closing—to avoid undefined behavior. Traditional solutions, such as runtime checks, documentation reliance, or ignoring error returns, introduce runtime overhead and potential for programmer oversight. NGrislain’s solution leverages Lean 4’s powerful type system to encode the socket state machine directly into the type definitions, effectively eliminating runtime checks without sacrificing correctness.

The approach centers around representing the socket state as an inductive type, defining five distinct states: `fresh`, `bound`, `listening`, `connected`, and `closed`. Each state corresponds to a stage in the socket lifecycle. The `decidableEq` tactic is employed to establish equality between these states, enabling automated reasoning within the type system. A core component of the system is the `Socket` structure, which encapsulates a raw socket handle (obtained via `lean_alloc_external`) and retains the socket’s state as a phantom parameter. Critically, this state information is erased at runtime, resulting in identical memory layouts for sockets in the same state, thereby minimizing overhead. The constructor for the `Socket` structure is made protected to further enforce state consistency.

The system employs a function-based approach to define operations like `socket`, `bind`, `listen`, `accept`, `connect`, `send`, `recv`, and `close`. Each function is meticulously designed to declare pre- and post-state conditions, enforced through dependent types. For example, the `send` function requires a `Socket` in the `connected` state, triggering a type error immediately if the function is called on a `Socket` in the `fresh` state. This rigorous type checking is performed during compilation, eliminating the need for runtime assertions or exception handling. The `close` function utilizes a dependent type constraint (`state ≠ .closed`) to prevent double-closing of the socket, a common source of errors. When the constraint is violated (attempting to close a socket already in the `closed` state), the program immediately halts with an error.

The implementation incorporates seventeen distinct theorems, formally proving that all five socket states are pairwise distinct; these theorems, verified using the `decide` tactic, are incorporated to provide additional clarity without impacting performance. Lean 4’s type system guarantees that the generated C code will be identical to raw C code, achieving true zero-cost POSIX compliance—no branching, no flags, no state fields are introduced, substantially enhancing performance.

A comparison of the proposed implementation with alternative approaches highlights its efficiency. Compared to runtime check-based solutions (e.g., Python, Java, Go), which typically incur approximately 50 branches per call, Lean 4’s approach delivers zero branches. Compared to Rust’s typestate-based approach, which also avoids runtime checks, Lean 4’s method represents a significant shift, moving the state-checking process directly into the type system, offering a theoretical runtime cost of approximately 300 (though the actual cost is effectively zero in practice due to the compile-time verification). The approach contrasts sharply with traditional C implementations, which rely on manual checks and error returns, often leading to undefined behavior.

The detailed explanation features illustrative examples, including several commented-out code snippets demonstrating potential errors and the subsequent type-checking errors produced by the Lean 4 kernel. These examples serve as a practical demonstration of the system’s effectiveness and robust error detection capabilities. The document underscores the unique characteristic of Lean 4’s approach—the proof obligation `state ≠ .closed` is a genuine logical proposition verified by the kernel, unlike heuristics or linting rules. This verification process is seamlessly integrated into the compilation stage and then discarded, guaranteeing execution speed equivalent to raw C. The overall methodology effectively embodies a mathematical verification of the socket protocol’s compliance rules within the type system.