Utcpµ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).
TCP is mainly specified in RFC 9293.
val empty : (unit -> 'a) -> string -> 'a stateempty make_notify id constructs an empty TCP state with a function how to create a notifications, and an identifier for the TCP stack.
start_listen t port adds port to the set of listened to ports.
stop_listen t port removes port from the set of listened to ports.
peers flow is the two endpoints of the flow, each identifiable by their IP and port.
module Sequence : sig ... endThe module of TCP sequence numbers (unsigned 32 bit values, arithmetic operations may wrap)
module Segment : sig ... endThe module of TCP segments, as seen on the wire.
The type for outputting packets: a triple of source IP address, destination IP address, and segment.
val timer :
'a state ->
Mtime.t ->
'a state
* (flow
* [ `Retransmission_exceeded
| `Timer_2msl
| `Timer_connection_established
| `Timer_fin_wait_2 ]
* 'a
* 'a)
list
* output listtimer 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.
val handle_buf :
'a state ->
Mtime.t ->
src:Ipaddr.t ->
dst:Ipaddr.t ->
Cstruct.t ->
'a state
* [ `Established of flow * 'a option
| `Drop of flow * 'a option * 'a list
| `Signal of flow * 'a list ]
option
* output listhandle_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.
val connect :
src:Ipaddr.t ->
?src_port:int ->
dst:Ipaddr.t ->
dst_port:int ->
'a state ->
Mtime.t ->
'a state * flow * 'a * outputconnect ~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.
val close :
'a state ->
Mtime.t ->
flow ->
('a state * output list, [ `Not_found | `Msg of string ]) resultclose 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).
val shutdown :
'a state ->
Mtime.t ->
flow ->
[ `read | `write | `read_write ] ->
('a state * output list, [ `Not_found | `Msg of string ]) resultshutdown 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.
val recv :
'a state ->
Mtime.t ->
flow ->
('a state * string list * 'a * output list,
[ `Not_found | `Msg of string | `Eof ])
resultrecv state now flow receives data for flow. The read notification is also provided - if there's no awaiting data, this notification can be waited on.
val send :
'a state ->
Mtime.t ->
flow ->
?off:int ->
?len:int ->
string ->
('a state * int * 'a * output list, [ `Not_found | `Msg of string ]) resultsend 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.
val force_enqueue :
'a state ->
Mtime.t ->
flow ->
?off:int ->
?len:int ->
string ->
('a state, [ `Not_found | `Msg of string ]) resultforce_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.