µTCP - an implementation of the Transmission Control Protocol
TCP is a widely used protocol on the Internet. µTCP has its origins in the Netsem (network semantics) research project, which is an executable specification of TCP/IP and the Unix sockets API in HOL4.
µTCP was manually translated from the HOL4 specification into OCaml, and decisions were taken where needed. There is no support for out of band data (urgent pointers). TCP timestamps are also not supported (due to its dubious use).
The module of TCP sequence numbers (unsigned 32 bit values, arithmetic operations may wrap), comparison adheres to serial number arithmetics from RFC 1982.
The type for outputting packets: a triple of source IP address, destination IP address, and segment.
Sourceval timer :
'astate->Mtime.t->'astate
* (flow
* [ `Retransmission_exceeded
| `Timer_2msl| `Timer_connection_established| `Timer_fin_wait_2 ]
* 'a
* 'a)
list
* output list
timer state now runs the TCP timer at now for state. It results in a new state, a list of errors (a quadruple of flow, concrete error, and receive and send notification), and a list of segments to send out.
handle_buf state now ~src ~dst buf handles the buffer buf for the TCP stack. This results in a fresh state, optionally a change in the flow (Established, Drop, Signal), and a list of segments to send.
connect ~src ?src_port ~dst ~dst_port state now starts a TCP connection from src, src_port to dst, dst_port. The src_port will be picked at random if not provided. The output is a fresh TCP state, the flow, a notification, and a segment to send out.
close state now flow closes flow. It results either in a fresh TCP state and a list of segments to send out, or an error (if the flow cannot be found, or some other error).
shutdown state now flow direction shuts the flow down in the given direction. It results in a frsh TCP state and a list of segments to send out, or an error.
send state now flow ~off ~len data sends data on flow, starting at off (defaults to 0) of length len (defaults to data until the end). This outputs a fresh TCP state, the number of bytes enqueued, the write notification, and a list of segments to send.
force_enqueue state now flow ~off ~len data pushes data on flow, starting at off (defaults to 0) of length len (defaults to data until the end) onto the send queue. This may exceed the send queue size, use with caution.