Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

ngrislain.github.io

Post reply on HN
Print view View original

11–20 of 24 posts

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

#11

Post by hackyhacky »

yjftsjthsd-h wrote: post #2

> 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. Couldn't you do that in a more conventional type/class system without using an actual proof system? Instead of there being a Socket type/class, just make a Socket_Fresh, Socket_Bound, Socket_Listening, Socket_Connected, and maybe Socket_Closed (not 100% sur…

That wouldn't work because there would be nothing stopping you from re-using a value representing an old state.

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

#12

Post by comex »

russdill wrote: post #9

This is a based on such a surface level understanding of one type of posix socket. Calling close twice on a socket is a normal allowed thing, particularly for non blocking sockets. Datagram sockets can be operated with bind, without bind, with connect and bind and with both called multiple times.

Some of what you said is true, but you definitely can’t call close multiple times on the same file descriptor. close always immediately drops the file descriptor and isn’t like non-blocking socket operations that you have to try repeatedly until they succeed. You could, however, create multiple file descriptors pointing to the same socket with dup or other methods, in which case you’d need to close all of them to disconnect the socket.

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

#13

Post by 12_throw_away »

I'm like 3 sentences in and already things do not quite make sense.

> Calling [socket] operations in the wrong order [...] is undefined behaviour in C.

UB? For using a socket incorrectly? You sure about that?

> Documentation — trust the programmer to read the man page (C, Rust).

I'm sorry, are they saying that rust's socket interface is unsound? Looks to me like it's a pretty standard Rust-style safe interface [1], what am I missing?

[1] https://doc.rust-lang.org/std/net/struct.TcpListener.html

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

#15

Post by russdill »

comex wrote: post #12
russdill wrote: post #9

This is a based on such a surface level understanding of one type of posix socket. Calling close twice on a socket is a normal allowed thing, particularly for non blocking sockets. Datagram sockets can be operated with bind, without bind, with connect and bind and with both called multiple times.

Some of what you said is true, but you definitely can’t call close multiple times on the same file descriptor. close always immediately drops the file descriptor and isn’t like non-blocking socket operations that you have to try repeatedly until they succeed. You could, however, create multiple file descriptors pointing to the same socket with dup or other methods, in which case you’d need to close all of them to dis…

Bah, I was thinking of shutdown

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

#16

Post by WhyNotHugo »

12_throw_away wrote: post #13

I'm like 3 sentences in and already things do not quite make sense. > Calling [socket] operations in the wrong order [...] is undefined behaviour in C. UB? For using a socket incorrectly? You sure about that? > Documentation — trust the programmer to read the man page (C, Rust). I'm sorry, are they saying that rust's socket interface is unsound? Looks to me like it's a pretty standard Rust-style safe interface [1], w…

They say “undefined behaviour”. They mean “returns an error”, or “can return an error”.

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

#17

Post by tom_ »

12_throw_away wrote: post #13

I'm like 3 sentences in and already things do not quite make sense. > Calling [socket] operations in the wrong order [...] is undefined behaviour in C. UB? For using a socket incorrectly? You sure about that? > Documentation — trust the programmer to read the man page (C, Rust). I'm sorry, are they saying that rust's socket interface is unsound? Looks to me like it's a pretty standard Rust-style safe interface [1], w…

The C standard doesn't have anything to say about sockets at all, so not like it's defined to use them even in the right order.

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

#18

Post by ridiculous_fish »

hackyhacky wrote: post #11
yjftsjthsd-h wrote: post #2

> 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. Couldn't you do that in a more conventional type/class system without using an actual proof system? Instead of there being a Socket type/class, just make a Socket_Fresh, Socket_Bound, Socket_Listening, Socket_Connected, and maybe Socket_Closed (not 100% sur…

That wouldn't work because there would be nothing stopping you from re-using a value representing an old state.

That's exactly what affine / linear types do.

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

#19

Post by jibal »

paulddraper wrote: post #3
yjftsjthsd-h wrote: post #2

> 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. Couldn't you do that in a more conventional type/class system without using an actual proof system? Instead of there being a Socket type/class, just make a Socket_Fresh, Socket_Bound, Socket_Listening, Socket_Connected, and maybe Socket_Closed (not 100% sur…

The innovation is making that have zero runtime cost. (Though to be fair, I doubt the runtime cost is really significant...)

That's very odd response if you know what a type system is.

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

#20

Post by singron »

e-dant wrote: post #6

This is cool stuff, but a nitpick: It’s not undefined behavior in the language sense in C to do socket ops on a bad file descriptor. It’s just an error from the kernel’s point of view, and the kernel will throw -errno at you.

Yes it's not UB, but the consequences are not limited to a EINVAL/EBADF/EBADFD. Calling close twice is essentially the same problem as calling free twice, so you get all the use-after-free problems on your file descriptors.
Post reply on HN