Module 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.

Abstract state type

type 'a state

The abstract type of an immutable state of the TCP stack.

val empty : (unit -> 'a) -> string -> 'a state

empty make_notify id constructs an empty TCP state with a function how to create a notifications, and an identifier for the TCP stack.

val start_listen : 'a state -> int -> 'a state

start_listen t port adds port to the set of listened to ports.

val stop_listen : 'a state -> int -> 'a state

stop_listen t port removes port from the set of listened to ports.

type flow

The abstract type of a flow - a connection between this TCP stack and a remote endpoint.

val pp_flow : flow Fmt.t

pp_flow flow pretty-prints the flow.

val peers : flow -> (Ipaddr.t * int) * (Ipaddr.t * int)

peers flow is the two endpoints of the flow, each identifiable by their IP and port.

module Sequence : sig ... end

The module of TCP sequence numbers (unsigned 32 bit values, arithmetic operations may wrap)

module Segment : sig ... end

The module of TCP segments, as seen on the wire.

type output = Ipaddr.t * Ipaddr.t * Segment.t

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 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.

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 list

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.

val connect : src:Ipaddr.t -> ?src_port:int -> dst:Ipaddr.t -> dst_port:int -> 'a state -> Mtime.t -> 'a state * flow * 'a * output

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.

val close : 'a state -> Mtime.t -> flow -> ('a state * output list, [ `Not_found | `Msg of string ]) result

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).

val shutdown : 'a state -> Mtime.t -> flow -> [ `read | `write | `read_write ] -> ('a state * output list, [ `Not_found | `Msg of string ]) result

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.

val recv : 'a state -> Mtime.t -> flow -> ('a state * string list * 'a * output list, [ `Not_found | `Msg of string | `Eof ]) result

recv 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 ]) result

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.

val force_enqueue : 'a state -> Mtime.t -> flow -> ?off:int -> ?len:int -> string -> ('a state, [ `Not_found | `Msg of string ]) result

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.