Quic loss recovery

include quic_types
include quic_application
include quic_security
include quic_frame
include quic_packet
include quic_locale

include quic_types include quic_packet include quic_transport_error_code include quic_frame

module quic_packet_arr(quic_packet) = { instance jdx : unbounded_sequence instance arr : array(jdx,quic_packet) }

instance quic_packet : quic_packet_arr(quic_packet)

QUIC uses separate packet number spaces for each encryption level, except 0-RTT and all generations of 1-RTT keys use the same packet number space. Separate packet number spaces ensures that the acknowledgment of packets sent with one level of encryption will not cause spurious retransmission of packets sent with a different encryption level. Congestion control and round-trip time (RTT) measurement are unified across packet number spaces

QUIC separates transmission order from delivery order: packet numbers indicate transmission order, and delivery order is determined by the stream offsets in STREAM frames.

QUIC's packet number is strictly increasing within a packet number space and directly encodes transmission order. A higher packet number signifies that the packet was sent later, and a lower packet number signifies that the packet was sent earlier.

QUIC starts a loss epoch when a packet is lost. The loss epoch ends when any packet sent after the start of the epoch is acknowledged

function loss_epoch : microseconds

Multi-modal timer used for loss detection

function loss_detection_timer : microseconds

QUIC endpoints measure the delay incurred between when a packet is received and when the corresponding acknowledgment is sent, allowing a peer to maintain a more accurate RTT estimate; see Section 13.2 of [QUIC-TRANSPORT]. At a high level, an endpoint measures the time from when a packet was sent to when it is acknowledged as an RTT sample.

function first_rtt_sample : microseconds

Note: we do all the calculation in microseconds, but the result is in milliseconds. Why ? to avoid loosing precision when dividing by 1000 An endpoint computes the following three values for each path

function latest_rtt(C:cid) : microseconds

smoothed_rtt is an exponentially-weighted moving average of an endpoint's RTT samples, When there are no samples for a network path, and on the first RTT sample for the network path: smoothed_rtt = rtt_sample rttvar = rtt_sample / 2 On subsequent RTT samples, smoothed_rtt and rttvar evolve as follows: ack_delay = min(Ack Delay in ACK Frame, max_ack_delay) adjusted_rtt = latest_rtt if (min_rtt + ack_delay < latest_rtt): adjusted_rtt = latest_rtt - ack_delay smoothed_rtt = 7/8 * smoothed_rtt + 1/8 * adjusted_rtt rttvar_sample = abs(smoothed_rtt - adjusted_rtt) rttvar = 3/4 * rttvar + 1/4 * rttvar_sample

function smoothed_rtt(C:cid) : microseconds

and rttvar is the variation in the RTT samples, estimated using a mean variation.

function rttvar(C:cid) : microseconds

min_rtt is the minimum RTT observed for a given network path. min_rtt is set to the latest_rtt on the first RTT sample, and to the lesser of min_rtt and latest_rtt on subsequent samples. In this document, min_rtt is used by loss detection to reject implausibly small rtt samples.

function min_rtt(C:cid) : microseconds

The time the most recent ack-eliciting packet was sent.

function time_of_last_ack_eliciting_packet(E: quic_packet_type) : microseconds

The largest packet number acknowledged in the packet number space so far.

function largest_acked_packet(E: quic_packet_type) : pkt_num

function local_largest_acked_packet(E: quic_packet_type) : pkt_num

The time at which the next packet in that packet number space can be considered lost based on exceeding the reordering window in time

function loss_time(E: quic_packet_type) : microseconds

An association of packet numbers in a packet number space to information about them. sent_packets[pn_space][packet_number].packet_number = packet_number sent_packets[pn_space][packet_number].time_sent = now() sent_packets[pn_space][packet_number].ack_eliciting = ack_eliciting sent_packets[pn_space][packet_number].in_flight = in_flight sent_packets[pn_space][packet_number].sent_bytes = sent_bytes

TODO error: cannot determine an iteration bound for loop over quic_packet.idx function sent_packets(E: quic_packet_type) : quic_packet.arr

function newly_acked_packets(E: quic_packet_type, I:stream_pos) : quic_packet
function newly_acked_packets_end(E: quic_packet_type) : stream_pos

function lost_packets(E: quic_packet_type, I:stream_pos) : quic_packet
function lost_packets_end(E: quic_packet_type) : stream_pos

function pc_lost(E: quic_packet_type, I:stream_pos) : quic_packet
function pc_lost_end(E: quic_packet_type) : stream_pos

function sent_packets(E: quic_packet_type, I:stream_pos) : quic_packet
function sent_packets_end(E: quic_packet_type) : stream_pos
function sent_packets_packet_number(E: quic_packet_type,S: pkt_num) : pkt_num
function sent_packets_time_sent(E: quic_packet_type,S: pkt_num) : microseconds
relation sent_packets_ack_eliciting(E: quic_packet_type,S: pkt_num)
relation sent_packets_in_flight(E: quic_packet_type,S: pkt_num)
function sent_packets_sent_bytes(E: quic_packet_type,S: pkt_num) : stream_pos # frame.arr


function received_packets(E: quic_packet_type, I:stream_pos) : quic_packet
function received_packets_end(E: quic_packet_type) : stream_pos
function received_packets_packet_number(E: quic_packet_type,S: pkt_num) : pkt_num
function received_packets_time_sent(E: quic_packet_type,S: pkt_num) : microseconds
relation received_packets_ack_eliciting(E: quic_packet_type,S: pkt_num)
relation received_packets_in_flight(E: quic_packet_type,S: pkt_num)
function received_packets_sent_bytes(E: quic_packet_type,S: pkt_num) : stream_pos # frame.arr

function packets_to_retransmit(E: quic_packet_type, I:stream_pos) : frame.arr
function packets_to_retransmit_end(E: quic_packet_type) : stream_pos

relation ack_eliciting_packet_in_flight
relation ack_eliciting_packet_in_flight_per_space(E: quic_packet_type)

QUIC uses a probe timeout (PTO; see Section 6.2), with a timer based on TCP's retransmission timeout (RTO) computation; see [RFC6298]. QUIC's PTO includes the peer's maximum expected acknowledgment delay instead of using a fixed minimum timeout. QUIC does not collapse the congestion window when the PTO expires, since a single packet loss at the tail does not indicate persistent congestion. Instead, QUIC collapses the congestion window when persistent congestion is declared; Since QUIC does not collapse the congestion window on a PTO expiration, a QUIC sender is not limited from sending more in-flight packets after a PTO expiration if it still has available congestion window. This occurs when a sender is application limited and the PTO timer expires. This is more aggressive than TCP's RTO mechanism when application limited, but identical when not application limited

function sent_time_of_largest_acked(S:pkt_num) : microseconds
function ack_time : microseconds

Maximum reordering in packets before packet threshold loss detection considers a packet lost. The value recommended in Section 6.1.1 is 3.

function kPacketThreshold : stream_pos

Therefore, after receiving packets from an address that is not yet validated, an endpoint MUST limit the amount of data it sends to the unvalidated address to three times the amount of data received from that address. This limit on the size of responses is known as the anti-amplification limit

relation anti_amplification_limit_reached

Maximum reordering in time before time threshold loss detection considers a packet lost. Specified as an RTT multiplier. The value recommended in Section 6.1.2 is 9/8 * 1000

function kTimeThreshold : microseconds

Timer granularity. This is a system-dependent value, and Section 6.1.2 recommends a value of 1 ms.

function kGranularity : microseconds

The RTT used before an RTT sample is taken. The value recommended in Section 6.2.2 is 333 ms.

function kInitialRtt : milliseconds

When an ack-eliciting packet is transmitted, the sender schedules a timer for the PTO period as follows: PTO = smoothed_rtt + max(4rttvar, kGranularity) + max_ack_delay The number of times a PTO has been sent without receiving an acknowledgment.

function pto_count : microseconds # for avoid to cast
function pto_timeout : microseconds
function pto_backoff : stream_pos

function max_idle_timeout_server : microseconds
function max_idle_timeout_client : microseconds
function max_idle_timeout_used : microseconds
function idle_timeout(C:cid) : microseconds
function timeout : microseconds
relation respect_idle_timeout
relation connection_timeout

function max_ack_delay_tp : microseconds
function local_max_ack_delay_tp : microseconds

function ack_delay_exponent_tp : microseconds
function local_ack_delay_exponent_tp : microseconds

validation_timeout = max(3PTO, 6*kInitialRtt)

function validation_timeout : microseconds

relation need_sent_ack_eliciting_initial_packet
relation need_sent_ack_eliciting_handshake_packet
relation need_sent_ack_eliciting_application_packet

QUIC allows probe packets to temporarily exceed the congestion window whenever the timer expires

Sending a single ack-eliciting packet also increases the chances of incurring additional latency when a receiver delays its acknowledgment. QUIC therefore recommends that the minimum congestion window be two packets. While this increases network load, it is considered safe since the sender will still reduce its sending rate exponentially under persistent congestion

function minimum_congestion_window : stream_pos

relation pn_space_discarded

relation is_idle

QUIC treats loss of a packet containing handshake data the same as other losses.

after init {
    need_sent_ack_eliciting_initial_packet := false;
    need_sent_ack_eliciting_handshake_packet := false;
    need_sent_ack_eliciting_application_packet := false;

    loss_detection_timer := 0;
    pto_count := 0;

    latest_rtt(C) := 0;
    smoothed_rtt(C) := 333000; # 333ms ~ kInitialRtt -> from handshake
    rttvar(C) := 165000;
    min_rtt(C) := 0;

    first_rtt_sample := 0;
    largest_acked_packet(E) := 0xFFFFFF; # infinity
    local_largest_acked_packet(E) := 0xFFFFFF; # infinity
    time_of_last_ack_eliciting_packet(E) := 0;
    loss_time(E) := 0;

    kPacketThreshold := 3;
    kTimeThreshold := 1125; #9/8;
    kGranularity := 1000; #1ms

    max_ack_delay_tp := 25000; # 25ms
    local_max_ack_delay_tp := 25000; # 25ms

    local_ack_delay_exponent_tp := 3;
    ack_delay_exponent_tp := 3;

    connection_timeout := false;
    respect_idle_timeout := true;
    minimum_congestion_window := 2;

    ack_eliciting_packet_in_flight := false;

    anti_amplification_limit_reached := false;

sent_packets(E) := quic_packet.arr.empty;

    sent_packets_end(E) := 0;
    newly_acked_packets_end(E) := 0;
    lost_packets_end(E) := 0;
    pc_lost_end(E) := 0;
    pn_space_discarded := false;
    is_idle := false;
}

import action show_latest_rtt(t:microseconds,c:cid)
import action show_min_rtt(t:microseconds,c:cid)
import action show_smoothed_rtt(t:microseconds,c:cid)
import action show_rttvar(t:microseconds,c:cid)

action pow(x:microseconds, y:microseconds) returns (z:microseconds) = {
    <<<
    z = pow(x,y);
    >>>
}

action abs(x:microseconds) returns (z:microseconds) = {
    <<<
    z = abs(x);
    >>>
}

QUIC loss detection uses a single timer for all timeout loss detection. The duration of the timer is based on the timer's mode, which is set in the packet and timer events further below. The function SetLossDetectionTimer defined below shows how the single timer is set.This algorithm may result in the timer being set in the past, particularly if timers wake up late. Timers set in the past fire immediately.Pseudocode for SetLossDetectionTimer follows (where the "^" operator represents exponentiation):

action get_pto_time_and_space(dst:ip.endpoint, dcid:cid) returns (pto_timeout_res:microseconds, pto_space:quic_packet_type) = {
    var max := 4 * rttvar(dcid);
    if max < kGranularity {
        max := kGranularity;
    }
    var duration := (smoothed_rtt(dcid) + max) * pow(pto_count,2);

Anti-deadlock PTO starts from the current time

    if ~ack_eliciting_packet_in_flight {
        if ~peer_completed_address_validation(dst, dcid) {
            pto_timeout_res := duration + time_api.c_timer.now_micros;
            if established_handshake_keys(dcid) {
                pto_space := quic_packet_type.handshake;
            }
            else {
                pto_space := quic_packet_type.initial;
            }
         };
    } else {

TODO should loop on all packet number spaces, but strange

        var temp_pto_timeout_res : microseconds := 0xFFFFFF; # infinity

        var temp_pto_space := quic_packet_type.initial;
        var t := time_of_last_ack_eliciting_packet(temp_pto_space) + duration;
        if t < temp_pto_timeout_res {
            pto_timeout_res := t;
            pto_space := temp_pto_space;
        };

        temp_pto_space := quic_packet_type.handshake;
        t := time_of_last_ack_eliciting_packet(temp_pto_space) + duration;
        if t < temp_pto_timeout_res {
            pto_timeout_res := t;
            pto_space := temp_pto_space;
        };

        temp_pto_space := quic_packet_type.one_rtt;
        if peer_completed_address_validation(dst, dcid) {
            duration := duration + max_ack_delay_tp * pow(pto_count,2);
            t := time_of_last_ack_eliciting_packet(temp_pto_space) + duration;
            if t < temp_pto_timeout_res {
                pto_timeout_res := t;
                pto_space := temp_pto_space;
            };
        };
    };
    call show_get_pto_time_and_space(pto_timeout_res, pto_space);
}

action get_loss_time_space returns (time:microseconds, space:quic_packet_type) = {
    var inter_time := loss_time(quic_packet_type.initial);
    var inter_space := quic_packet_type.initial;

    if inter_time = 0 | loss_time(quic_packet_type.handshake) < inter_time {
        inter_time := loss_time(quic_packet_type.handshake);
        inter_space := quic_packet_type.handshake;
    };

    if inter_time = 0 | loss_time(quic_packet_type.one_rtt) < inter_time {
        inter_time := loss_time(quic_packet_type.one_rtt);
        inter_space := quic_packet_type.one_rtt;
    };

    time := inter_time;
    space := inter_space;
}

action peer_completed_address_validation(dst:ip.endpoint, dcid:cid) returns (b:bool) = {
    if dst = server.ep {
        b := true;
    }
    b := established_handshake_keys(dcid); # has received Handshake ACK || handshake confirmed
}

action set_loss_detection_timer(dst:ip.endpoint, dcid: cid) = {
    var earliest_loss_time : microseconds;
    var space : quic_packet_type;
    (earliest_loss_time, space) := get_loss_time_space;
    call show_get_loss_time_space(earliest_loss_time, space);

    if earliest_loss_time ~= 0 {
        loss_detection_timer :=  earliest_loss_time;
    } else {
        if anti_amplification_limit_reached { # (dst, dcid)
           loss_detection_timer := 0;
        }
        else {
            if ~ack_eliciting_packet_in_flight & peer_completed_address_validation(dst, dcid) {

There is nothing to detect lost, so no timer is set. However, the client needs to arm the timer if the server might be blocked by the anti-amplification limit.

                loss_detection_timer := 0;
            } else {
                var pto_timeout_t : microseconds;
                var pto_space : quic_packet_type;
                (pto_timeout_t, pto_space) := get_pto_time_and_space(dst,dcid);
                loss_detection_timer := pto_timeout_t;
                pto_timeout := pto_timeout_t;
            }

        }
    };
    call show_loss_detection_timer(loss_detection_timer);
}

When the loss detection timer expires, the timer's mode determines the action to be performed.

action on_loss_detection_timeout(dst:ip.endpoint, dcid: cid) = {
    var earliest_loss_time : microseconds;
    var pn_space : quic_packet_type;
    (earliest_loss_time, pn_space) := get_loss_time_space;
    call show_get_loss_time_space(earliest_loss_time, pn_space);
    if earliest_loss_time ~= 0 {

var lost_packets :=

        detect_and_remove_lost_packets(pn_space,dcid);

assert(!lost_packets.empty())

        if lost_packets_end(pn_space) > 0 {
            call on_packets_lost(pn_space);
            call set_loss_detection_timer(dst, dcid);
        };
    } else {
        if ~ack_eliciting_packet_in_flight & ~peer_completed_address_validation(dst, dcid) {

Client sends an anti-deadlock packet: Initial is padded to earn more anti-amplification credit, a Handshake packet proves address ownership.

            if established_handshake_keys(dcid) {

TODO SendOneAckElicitingHandshakePacket()

                call show_need_sent_ack_eliciting_handshake_packet;
                need_sent_ack_eliciting_handshake_packet := true;
            } else {

TODO SendOneAckElicitingPaddedInitialPacket()

                call show_need_sent_ack_eliciting_initial_packet;
                need_sent_ack_eliciting_initial_packet := true;
            }
        } else {

PTO. Send new data if available, else retransmit old data. If neither is available, send a single PING frame.

            var pto_timeout_t : microseconds;
            var pto_space : quic_packet_type;
            (pto_timeout_t, pto_space) := get_pto_time_and_space(dst,dcid);
            loss_detection_timer := pto_timeout_t;
            pto_timeout := pto_timeout_t;

TODO SendOneOrTwoAckElicitingPackets(pn_space)

            if pn_space = quic_packet_type.initial {
                call show_need_sent_ack_eliciting_initial_packet;
                need_sent_ack_eliciting_initial_packet := true;
            } else if pn_space = quic_packet_type.handshake {
                call show_need_sent_ack_eliciting_handshake_packet;
                need_sent_ack_eliciting_handshake_packet := true;
            } else {
                call show_need_sent_ack_eliciting_application_packet;
                need_sent_ack_eliciting_application_packet := true;
            };
        };
        pto_count := pto_count + 1;
        call set_loss_detection_timer(dst, dcid);
    };
}

import action show_need_sent_ack_eliciting_initial_packet
import action show_need_sent_ack_eliciting_handshake_packet
import action show_need_sent_ack_eliciting_application_packet

DetectAndRemoveLostPackets is called every time an ACK is received or the time threshold loss detection timer expires. This function operates on the sent_packets for that packet number space and returns a list of packets newly detected as lost.

action detect_and_remove_lost_packets(pn_space:quic_packet_type, dcid:cid) = {
    loss_time(pn_space) := 0;
    var max := smoothed_rtt(dcid);
    if max < latest_rtt(dcid) {
        max := latest_rtt(dcid);
    };

    var loss_delay := kTimeThreshold * max;
    if loss_delay < kGranularity {
        loss_delay := kGranularity;
    };

    var tp := trans_params(dcid);

    var lost_sent_time := time_api.c_timer.now_micros - loss_delay;
    var sent_packets_size := sent_packets_end(pn_space);
    sent_packets_end(pn_space) := 0;
    lost_packets_end(pn_space) := 0;
    var idx : stream_pos := 0;
    call show_detect_and_remove_lost_packets(lost_sent_time, loss_delay, sent_packets_size);
    while idx < sent_packets_size {
        var current_pkt := sent_packets(pn_space,idx);

TODO

        if current_pkt.seq_num <= largest_acked_packet(pn_space) {
            if min_ack_delay.is_set(tp) {
                if sent_packets_time_sent(pn_space, current_pkt.seq_num) <= lost_sent_time |
                    largest_acked_packet(pn_space) >= current_pkt.seq_num + streampos_to_seqnum(ack_out_of_order_val(dcid)) {
                    lost_packets(pn_space,lost_packets_end(pn_space)) := current_pkt;
                    lost_packets_end(pn_space) := lost_packets_end(pn_space) + 1;
                }
                else {
                    sent_packets(pn_space,sent_packets_end(pn_space)) := current_pkt;
                    sent_packets_end(pn_space) := sent_packets_end(pn_space) + 1;
                    if loss_time(pn_space) = 0 {
                        loss_time(pn_space) := sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay;
                    }
                    else {
                        var min := loss_time(pn_space);
                        if min > sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay {
                            loss_time(pn_space) := sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay;
                        }
                    }
                };
            }
            else {
                if sent_packets_time_sent(pn_space, current_pkt.seq_num) <= lost_sent_time |
                    largest_acked_packet(pn_space) >= current_pkt.seq_num + streampos_to_seqnum(kPacketThreshold) {
                    lost_packets(pn_space,lost_packets_end(pn_space)) := current_pkt;
                    lost_packets_end(pn_space) := lost_packets_end(pn_space) + 1;
                } else {
                    sent_packets(pn_space,sent_packets_end(pn_space)) := current_pkt;
                    sent_packets_end(pn_space) := sent_packets_end(pn_space) + 1;
                    if loss_time(pn_space) = 0 {
                        loss_time(pn_space) := sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay;
                    }
                    else {
                        var min := loss_time(pn_space);
                        if min > sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay {
                            loss_time(pn_space) := sent_packets_time_sent(pn_space, current_pkt.seq_num) + loss_delay;
                        }
                    }
                };
            }
        };
        idx := idx + 1;
    };

lost_packets := lost_packets_temp;

    call show_loss_time_update(loss_time(pn_space), pn_space);
}

import action show_loss_time_update(t:microseconds, pn_space:quic_packet_type)

When a server is blocked by anti-amplification limits, receiving a datagram unblocks it, even if none of the packets in the datagram are successfully processed. In such a case, the PTO timer will need to be rearmed.

action on_datagram_received(dst:ip.endpoint, dcid:cid, datagram:stream_data) = {

If this datagram unblocks the server, arm the PTO timer to avoid deadlock.

    if anti_amplification_limit_reached { # TODO
        call set_loss_detection_timer(dst, dcid);
        if loss_detection_timer < time_api.c_timer.now_micros {
            loss_detection_timer := pto_timeout;

Execute PTO if it would have expired while the amplification limit applied.

            call show_loss_detection_timeout;
            call on_loss_detection_timeout(dst, dcid);
        };
    };
}

import action show_loss_detection_timeout

DetectAndRemoveAckedPackets finds packets that are newly acknowledged and removes them from sent_packets.

action detect_and_remove_acked_packets(largest_acked:pkt_num, pn_space:quic_packet_type) = {
    var sent_packets_size := sent_packets_end(pn_space);
    sent_packets_end(pn_space) := 0;
    newly_acked_packets_end(pn_space) := 0;
    var idx : stream_pos := 0;
    if sent_packets_size > 0 {
        while idx < sent_packets_size {
            var current_pkt := sent_packets(pn_space,idx);
            if current_pkt.seq_num <= largest_acked {

acked

                newly_acked_packets(pn_space,newly_acked_packets_end(pn_space)) := current_pkt;
                newly_acked_packets_end(pn_space) := newly_acked_packets_end(pn_space) + 1;
            }
            else {

not acked

                sent_packets(pn_space,sent_packets_end(pn_space)) := current_pkt;
                sent_packets_end(pn_space) := sent_packets_end(pn_space) + 1;
            }
            idx := idx + 1;
        };
    };
    call show_detect_and_remove_acked_packets(largest_acked, sent_packets_size, newly_acked_packets_end(pn_space), sent_packets_end(pn_space));
}

When an ACK frame is received, it may newly acknowledge any number of packets.

action on_ack_received(dst:ip.endpoint, largest_acked:pkt_num, ack_delay:microseconds, pn_space:quic_packet_type) = {
    call show_on_ack_received(largest_acked, ack_delay, pn_space);
    ack_delay := ack_delay * pow(2, ack_delay_exponent_tp);
    call show_on_ack_received(largest_acked, ack_delay, pn_space);
    if largest_acked_packet(pn_space) = 0xFFFFFF { # infinity
        largest_acked_packet(pn_space) := largest_acked;
    } else {
        if largest_acked > largest_acked_packet(pn_space) {
            largest_acked_packet(pn_space) := largest_acked;
        }
    }

call show_largest_acked_packet(largest_acked, pn_space); DetectAndRemoveAckedPackets finds packets that are newly acknowledged and removes them from sent_packets.

    detect_and_remove_acked_packets(largest_acked, pn_space);

    if newly_acked_packets_end(pn_space) > 0 {

Update the RTT if the largest acknowledged is newly acked and at least one ack-eliciting was newly acked.

        var idx : stream_pos:= 0;
        var largest_acked_pkt := newly_acked_packets(pn_space, idx);
        idx := idx + 1;
        while idx < newly_acked_packets_end(pn_space) {
            if newly_acked_packets(pn_space, idx).seq_num > largest_acked_pkt.seq_num {
                largest_acked_pkt := newly_acked_packets(pn_space, idx);
            }
            idx := idx + 1;
        }
        call show_largest_acked_packet(largest_acked_pkt.seq_num, largest_acked, pn_space);
        call show_include_ack_eliciting(includes_ack_eliciting(pn_space), pn_space);
        if largest_acked_pkt.seq_num = largest_acked & includes_ack_eliciting(pn_space) {
            latest_rtt(largest_acked_pkt.dst_cid) := time_api.c_timer.now_micros - sent_packets_time_sent(largest_acked_pkt.ptype,largest_acked_pkt.seq_num);
            call show_latest_rtt(latest_rtt(largest_acked_pkt.dst_cid),largest_acked_pkt.dst_cid);
            call update_rtt(ack_delay, largest_acked_pkt.dst_cid);
        }

Process ECN information if present. TODO if ack.ecn { # TODO call process_ecn(ack,pn_space); }

        detect_and_remove_lost_packets(pn_space,largest_acked_pkt.dst_cid);
        call show_detect_and_remove_lost_packets_size(pn_space,lost_packets_end(pn_space));
        if lost_packets_end(pn_space) > 0 {
            call on_packets_lost(pn_space);
        }

        call on_packets_acked(pn_space);

Reset pto_count unless the client is unsure if the server has validated the client's address.

        if peer_completed_address_validation(dst, largest_acked_pkt.dst_cid) {
            pto_count := 0;
        }
        call set_loss_detection_timer(dst, largest_acked_pkt.dst_cid);
    }
}

import action show_detect_and_remove_lost_packets_size(pn_space:quic_packet_type,lost_packets_end:stream_pos)
import action show_on_ack_received(largest_acked:pkt_num, ack_delay:microseconds, pn_space:quic_packet_type)

action on_ack_sent(largest_acked:pkt_num, pn_space:quic_packet_type)  returns (ack_delay:microseconds) = {

An endpoint measures the delays intentionally introduced between the time the packet with the largest packet number is received and the time an acknowledgment is sent.

    var ack_sent_time := time_api.c_timer.now_micros;
    var ack_delay_non_encoded := received_packets_time_sent(pn_space,largest_acked) - ack_sent_time;
    ack_delay := ack_delay_non_encoded / pow(2, local_ack_delay_exponent_tp);
    call show_on_ack_sent(largest_acked, ack_delay,ack_sent_time, ack_delay_non_encoded, pn_space, pow(2, local_ack_delay_exponent_tp));
}

import action show_on_ack_sent(largest_acked:pkt_num, ack_delay:microseconds, ack_delasy:microseconds, ack_delay_non_encoded:microseconds, pn_space:quic_packet_type, pow_ack_delay_exponent_tp:microseconds)

action includes_ack_eliciting(pn_space:quic_packet_type) returns (res:bool) = {
    var idx : stream_pos := 0;
    var res_inter := false;
    while idx < newly_acked_packets_end(pn_space) {
        if sent_packets_ack_eliciting(newly_acked_packets(pn_space, idx).ptype, newly_acked_packets(pn_space, idx).seq_num) {
            res_inter := true;
        }
        idx := idx + 1;
    }
    res := res_inter;
}

action update_rtt(ack_delay:microseconds, dcid:cid) = {
    call show_update_rtt(latest_rtt(dcid), min_rtt(dcid), smoothed_rtt(dcid), rttvar(dcid), dcid);
    if first_rtt_sample = 0 {
        min_rtt(dcid) := latest_rtt(dcid);
        smoothed_rtt(dcid) := latest_rtt(dcid);
        rttvar(dcid) := latest_rtt(dcid) / 2;
        first_rtt_sample := time_api.c_timer.now_micros;
    } else {

min_rtt ignores acknowledgment delay.

        if min_rtt(dcid) > latest_rtt(dcid) {
            min_rtt(dcid) := latest_rtt(dcid);
        }

Limit ack_delay by max_ack_delay after handshake confirmation.

        if established_handshake_keys(dcid) {
            if ack_delay > max_ack_delay_tp {
                ack_delay := max_ack_delay_tp;
            }
        }

Adjust for acknowledgment delay if plausible.

        var adjusted_rtt := latest_rtt(dcid);
        if latest_rtt(dcid) > min_rtt(dcid) + ack_delay {
            adjusted_rtt := latest_rtt(dcid) - ack_delay;
        }
        var abs := abs(smoothed_rtt(dcid) - adjusted_rtt);

if smoothed_rtt(dcid) < adjusted_rtt { abs := abs * -1; }

        rttvar(dcid) := 3 * rttvar(dcid)/4 + abs/4;
        smoothed_rtt(dcid) := 7 * smoothed_rtt(dcid)/8 + adjusted_rtt/8;
    }

call show_latest_rtt(latest_rtt(dcid), dcid); call show_min_rtt(min_rtt(dcid), dcid); call show_smoothed_rtt(smoothed_rtt(dcid), dcid); call show_rttvar(rttvar(dcid), dcid);

    call show_update_rtt(latest_rtt(dcid), min_rtt(dcid), smoothed_rtt(dcid), rttvar(dcid), dcid);
}

import action show_update_rtt(latest_rtt:microseconds, min_rtt:microseconds, smoothed_rtt:microseconds, rttvar:microseconds, dcid:cid)

When Initial or Handshake keys are discarded, packets from the space are discarded and loss detection state is updated.

action on_pn_space_discarded(dst:ip.endpoint, dcid:cid, pn_space:quic_packet_type) = {
    if ~ pn_space_discarded {
        call remove_from_bytes_in_flight(pn_space);
        sent_packets_end(pn_space) := 0;

Reset the loss detection and PTO timer

        time_of_last_ack_eliciting_packet(pn_space) := 0;
        loss_time(pn_space) := 0;
        pto_count := 0;
        call show_on_pn_space_discarded(pn_space);
        call set_loss_detection_timer(dst, dcid);
        pn_space_discarded := true;
    }
}

import action show_on_pn_space_discarded(pn_space:quic_packet_type)

After a packet is sent, information about the packet is stored. The parameters to OnPacketSent are described in detail above in Appendix A.1.1.

action on_packet_sent(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet, sent_bytes:stream_pos) = {
    sent_time_of_largest_acked(pkt.seq_num) := time_api.c_timer.now_micros;

After a packet is sent, information about the packet is stored

    sent_packets_end(pkt.ptype) := sent_packets_end(pkt.ptype) + 1;
    sent_packets(pkt.ptype,sent_packets_end(pkt.ptype)) := pkt;
    sent_packets_packet_number(pkt.ptype,pkt.seq_num) := pkt.seq_num;
    sent_packets_time_sent(pkt.ptype,pkt.seq_num) := time_api.c_timer.now_micros;
    sent_packets_ack_eliciting(pkt.ptype,pkt.seq_num) := queued_ack_eliciting_pkt(seqnum_to_streampos(pkt.seq_num));
    sent_packets_in_flight(pkt.ptype,pkt.seq_num) := true;
    sent_packets_sent_bytes(pkt.ptype,pkt.seq_num) := sent_bytes; # TODO

    var idx : stream_pos := 0;
    ack_eliciting_packet_in_flight := false;
    ack_eliciting_packet_in_flight_per_space(pkt.ptype) := false;
    while idx < sent_packets_end(pkt.ptype) {
        if queued_ack_eliciting_pkt(seqnum_to_streampos(sent_packets(pkt.ptype,idx).seq_num)) {
            ack_eliciting_packet_in_flight := true;
            ack_eliciting_packet_in_flight_per_space(pkt.ptype) := true;
        }
        idx := idx + 1;
    }

    if queued_ack_eliciting_pkt(seqnum_to_streampos(pkt.seq_num)){
        time_of_last_ack_eliciting_packet(pkt.ptype) := time_api.c_timer.now_micros;
        bytes_in_flight := bytes_in_flight + sent_bytes;
    }
    call show_seqnum_to_streampos(seqnum_to_streampos(pkt.seq_num));
    call show_on_packet_sent(sent_packets_end(pkt.ptype), sent_packets_packet_number(pkt.ptype,pkt.seq_num), sent_packets_time_sent(pkt.ptype,pkt.seq_num), sent_packets_ack_eliciting(pkt.ptype,pkt.seq_num), sent_packets_in_flight(pkt.ptype,pkt.seq_num), sent_packets_sent_bytes(pkt.ptype,pkt.seq_num), ack_eliciting_packet_in_flight);
    call show_time_of_last_ack_eliciting_packet(time_of_last_ack_eliciting_packet(pkt.ptype),pkt.ptype);
    call set_loss_detection_timer(dst, pkt.dst_cid);
}

action on_packet_received(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet, sent_bytes:stream_pos) = {

After a packet is recv, information about the packet is stored

    received_packets_end(pkt.ptype) := received_packets_end(pkt.ptype) + 1;
    received_packets(pkt.ptype,received_packets_end(pkt.ptype)) := pkt;
    received_packets_packet_number(pkt.ptype,pkt.seq_num) := pkt.seq_num;
    received_packets_time_sent(pkt.ptype,pkt.seq_num) := time_api.c_timer.now_micros;
    received_packets_ack_eliciting(pkt.ptype,pkt.seq_num) := queued_ack_eliciting_pkt(seqnum_to_streampos(pkt.seq_num));
    received_packets_in_flight(pkt.ptype,pkt.seq_num) := true;
    received_packets_sent_bytes(pkt.ptype,pkt.seq_num) := sent_bytes; # TODO

    call show_seqnum_to_streampos(seqnum_to_streampos(pkt.seq_num));
    call show_on_packet_received(received_packets_end(pkt.ptype), received_packets_packet_number(pkt.ptype,pkt.seq_num), received_packets_time_sent(pkt.ptype,pkt.seq_num), received_packets_ack_eliciting(pkt.ptype,pkt.seq_num), sent_packets_in_flight(pkt.ptype,pkt.seq_num), received_packets_sent_bytes(pkt.ptype,pkt.seq_num));
}

import action show_get_loss_time_space(t:microseconds, s:quic_packet_type)
import action show_detect_and_remove_lost_packets(lost_sent_time:microseconds, loss_delay:microseconds, sent_packets_size:stream_pos)
import action show_detect_and_remove_acked_packets(largest_acked:pkt_num, sent_packets_size:stream_pos, newly_acked_packets_end:stream_pos, sent_packets_end:stream_pos)
import action show_on_packet_sent(sent_packets_end:stream_pos, sent_packets_packet_number:pkt_num, sent_packets_time_sent:microseconds, sent_packets_ack_eliciting:bool, sent_packets_in_flight:bool, sent_packets_sent_bytes:stream_pos, ack_eliciting_packet_in_flight:bool)
import action show_on_packet_received(sent_packets_end:stream_pos, sent_packets_packet_number:pkt_num, sent_packets_time_sent:microseconds, sent_packets_ack_eliciting:bool, sent_packets_in_flight:bool, sent_packets_sent_bytes:stream_pos)

import action show_include_ack_eliciting(res:bool, pn_space:quic_packet_type)
import action show_largest_acked_packet(largest_acked:pkt_num, largest_acked2d:pkt_num, pn_space:quic_packet_type)
import action show_loss_detection_timer(loss_detection_timer:microseconds)
import action show_get_pto_time_and_space(pto_timeout_res:microseconds, pto_space:quic_packet_type)
import action show_time_of_last_ack_eliciting_packet(time_of_last_ack_eliciting_packet:microseconds,ptype:quic_packet_type)