Move state machine to separate file and expand documentation

README.md

@@ -197,48 +197,7 @@ Now, again, this proposal does not specify if/how permission prompts should be i
 
 ### TCP State Machine
 
-The TCP valid states can be described by the following diagram:
-
-```mermaid
-stateDiagram-v2
-    [*] --> TCP_INIT: tcpSocketCreate()
-    [*] --> TCP_CONNECTION: accept()
-    TCP_INIT --> TCP_BIND: startBind()
-    TCP_BIND --> TCP_BIND_READY: granted
-    TCP_BIND --> TCP_INIT: denied
-    TCP_BIND_READY --> TCP_BOUND: finishBind()
-    TCP_BIND_READY --> TCP_ERROR: finishBind() error
-    TCP_INIT --> TCP_CONNECT: startConnect()
-    TCP_BOUND --> TCP_CONNECT: startConnect()
-    TCP_CONNECT --> TCP_CONNECT_READY: granted
-    TCP_CONNECT --> TCP_INIT: denied
-    TCP_CONNECT --> TCP_BOUND: denied
-    TCP_CONNECT_READY --> TCP_CONNECTION: finishConnect()
-    TCP_CONNECT_READY --> TCP_ERROR: finishConnect() error
-    TCP_BOUND --> TCP_LISTEN: startListen()
-    TCP_LISTEN --> TCP_LISTEN_READY: granted
-    TCP_LISTEN --> TCP_BOUND: denied
-    TCP_LISTEN_READY --> TCP_LISTENER: finishListen()
-    TCP_LISTEN_READY --> TCP_ERROR: finishListen() error
-    TCP_CONNECTION --> TCP_CONNECTION: shutdown()
-    TCP_CONNECTION --> TCP_ERROR: socket error
-    TCP_CONNECTION --> TCP_CLOSED: socket close
-    TCP_LISTENER --> TCP_ERROR: socket error
-    TCP_LISTENER --> TCP_CLOSED: socket close
-
-    TCP_BIND: TCP_BIND [WAIT]
-    TCP_CONNECT: TCP_CONNECT [WAIT]
-    TCP_LISTEN: TCP_LISTEN [WAIT]
-    TCP_LISTENER: TCP_LISTENER [WAIT]
-```
-
-where the given methods synchronously transition the state when they are called. All method calls not on these state transition paths throw `invalid-state` while remaining in the current state, therefore always being recoverable by not transitioning the socket into the error state. Permission denied errors are retriable if the permissions dynamically change, and do not transition into the socket error state.
-
-The `TCP_CONNECT_READY` and `TCP_LISTEN_READY` states should eagerly handle socket connection and socket listen calls respectively, so that the finish calls represent completion of the asynchronous operation. Implementations may perform blocking connect and listen in the `connectFinish` and `listenFinish` calls, but this is discouraged.
-
-The state of the pollable for the TCP state machine is `RESOLVED` in every state, except for when transitioning into those states with `[WAIT]` on them - `TCP_BIND`, `TCP_CONNECT`, `TCP_LISTEN` and `TCP_LISTENER`. These correspond to states that can be polled on for their transition into another state that is resolved. The `TCP_LISTENER` state is the only one where the state of the pollable is the state of the underlying socket. It will be `RESOLVED` if there is a pending backlog, and `WAIT` otherwise. This means it is possible for the `finishListen()` call to instantaneously transition the pollable back to resolved from the initial wait state of resolving into `TCP_LISTENER`. In the `TCP_CONECTION` state, data IO on the socket streams does not affect the pollable state on the socket resource, and because the pollable is resolved in this state, the socket close and error events are not pollable.
-
-The TCP socket can be dropped in all states, performing the necessary cleanup. There are no traps associated with any state transitions.
+See [Operational Semantics](./TcpSocketOperationalSemantics.md).
 
 ### Considered alternatives
 

TcpSocketOperationalSemantics.md

@@ -0,0 +1,111 @@
+# Operational semantics of WASI TCP sockets
+
+WASI TCP sockets must behave [as-if](https://en.wikipedia.org/wiki/As-if_rule) they are implemented using the state machine described in this document.
+
+## States
+> Note: These refer to the states of the TCP socket, not the [TCP connection](https://datatracker.ietf.org/doc/html/rfc9293#name-state-machine-overview)
+
+In pseudo code:
+
+```wit
+interface tcp {
+    variant state {
+        unbound,
+        bind-in-progress(bind-future),
+        bound,
+        listen-in-progress(listen-future),
+        listening(accept-stream),
+        connect-in-progress(connect-future),
+        connected,
+        closed,
+    }
+
+    type bind-future = future<result<_, error-code>>;
+    type listen-future = future<result<_, error-code>>;
+    type connect-future = future<result<tuple<input-stream, output-stream>, error-code>>;
+    type accept-stream = stream<result<tuple<tcp-socket, input-stream, output-stream>, error-code>>;
+}
+```
+
+## Pollable readiness
+As seen above, there can be at most one asynchronous operation in progress at any time. The socket's pollable ready state can therefore be unambiguously derived as follows:
+
+```rs
+fn ready() -> bool {
+    match state {
+        unbound => true,
+        bound => true,
+        connected => true, // To poll for I/O readiness, subscribe to the input and output streams.
+        closed => true,
+
+        // Assuming that `f.is-resolved` returns true when the
+        // future has completed, either successfully or with failure.
+        bind-in-progress(f) => f.is-resolved,
+        listen-in-progress(f) => f.is-resolved,
+        connect-in-progress(f) => f.is-resolved,
+
+        // Assuming that `s.has-pending-items` returns true when
+        // there is an item ready to be read from the stream.
+        listening(s) => s.has-pending-items,
+    }
+}
+```
+
+## Transitions
+The following diagram describes the exhaustive set of all possible state transitions:
+
+```mermaid
+stateDiagram-v2
+    state "unbound" as Unbound
+    state "bind-in-progress" as BindInProgress
+    state "bound" as Bound
+    state "listen-in-progress" as ListenInProgress
+    state "listening" as Listening
+    state "connect-in-progress" as ConnectInProgress
+    state "connected" as Connected
+    state "closed" as Closed
+
+    [*] --> Unbound: create-tcp-socket()\n#ok
+
+    Unbound --> BindInProgress: start-bind()\n#ok
+    Unbound --> Unbound: start-bind()\n#error
+    Unbound --> ConnectInProgress: start-connect()\n#ok
+    Unbound --> Closed: start-connect()\n#error
+
+    ConnectInProgress --> ConnectInProgress: finish-connect()\n#error(would-block)
+    ConnectInProgress --> Closed: finish-connect()\n#error(NOT would-block)
+    ConnectInProgress --> Connected: finish-connect()\n#ok
+
+    Connected --> Connected: shutdown()
+    Connected --> Closed: «connection terminated»
+    
+    BindInProgress --> BindInProgress: finish-bind()\n#error(would-block)
+    BindInProgress --> Unbound: finish-bind()\n#error(NOT would-block)
+    BindInProgress --> Bound: finish-bind()\n#ok
+
+    Bound --> ListenInProgress: start-listen()\n#ok
+    Bound --> Closed: start-listen()\n#error
+    Bound --> ConnectInProgress: start-connect()\n#ok
+    Bound --> Closed: start-connect()\n#error
+
+    ListenInProgress --> ListenInProgress: finish-listen()\n#error(would-block)
+    ListenInProgress --> Closed: finish-listen()\n#error(NOT would-block)
+    ListenInProgress --> Listening: finish-listen()\n#ok
+
+    Listening --> Listening: accept()
+```
+
+Most transitions are dependent on the result of the method. Legend:
+- `#ok`: this transition only applies when the method returns successfully.
+- `#error`: this transition only applies when the method returns a failure.
+- `#error(would-block)`: this transition only applies when the method returns the `would-block` error specifically.
+- `#error(NOT would-block)`: this transition only applies when the method returns an error other than `would-block`.
+- _(no annotation)_: Transition in unconditional.
+
+#### Not shown in the diagram:
+- All state transitions shown above are driven by the caller and occur synchronously during the method invocations. There's one exception: the `«connection terminated»` transition from `connected` to `closed`. This can happen when: the peer closed the connection, a network failure occurred, the connection timed out, etc.
+- While `shutdown` immediately closes the input and/or output streams associated with the socket, it does not affect the socket's own state as it just _initiates_ a shutdown. Only after the full shutdown sequence has been completed will the `«connection terminated»` transition be activated. (See previous item)
+- Calling a method from the wrong state returns `error(invalid-state)` and does not affect the state of the socket. A special case are the `finish-*` methods; those return `error(not-in-progress)` when the socket is not in the corresponding `*-in-progress` state.
+- This diagram only includes the methods that impact the socket's state. For an overview of all methods and their required states, see [tcp.wit](./wit/tcp.wit)
+- Client sockets returned by `accept()` are in immediately in the `connected` state.
+- A socket resource can be dropped in any state.