include collections include order

include quic_types
include quic_transport_error_code
include quic_frame
include quic_transport_parameters
include ip
include quic_fsm_sending
include quic_fsm_receiving

The packet protocol

The packet protocol has several funcitons including establishing connections and loss detection. Packets carry frames whihc implement many other funcition of QUIC.

QUIC Packets

This section defines the QUIC packet datatype. Packets are the basic unit of communication between endpoints. A packet may be encoded in either the long or the short format. There are packet types: initial, handshake, zero_rtt and one_rtt. The zero_rtt type is encoded in the short format, while others are encoded in the long format. Packets have associated source cid (long format only) and destination cid, protocol version (long format only), and a packet sequence number. An initial packet also has a retry token, which is a (possibly empty) sequence of bytes. The payload of the packet consists of a sequence of frames (see frame.ivy).

Todo

retry and one_rtt packet types

Packet

The type quic_packet represents packet.

The fields are:

• ptype: the packet type [2]
• pversion: the protocol version, if long format, else 0 [3]
• dst_cid: the destination cid [4]
• src_cid: the source cid, if long format, else 0 [5]
• token: the retry token (see section 4.4.1) [6]
• seq_num: the packet sequence number [7]
• payload: the payload, a sequence of frames [8]

object quic_packet = {

type this instance idx : unbounded_sequence instance arr : array(idx,this)

object quic_packet_initial = { variant this of quic_packet = struct { ptype : quic_packet_type, # [2] dst_cid : cid, # [4] src_cid : cid, # [5] seq_num : pkt_num, # [7] payload : frame.arr # [8] } }

object quic_packet_handshake = { variant this of quic_packet = struct { ptype : quic_packet_type, # [2] dst_cid : cid, # [4] src_cid : cid, # [5] seq_num : pkt_num, # [7] payload : frame.arr # [8] } }

object quic_packet_one_rtt = { variant this of quic_packet = struct { ptype : quic_packet_type, # [2] dst_cid : cid, # [4] src_cid : cid, # [5] seq_num : pkt_num, # [7] payload : frame.arr # [8] } }

object quic_packet_zero_rtt = { variant this of quic_packet = struct { ptype : quic_packet_type, # [2] dst_cid : cid, # [4] src_cid : cid, # [5] seq_num : pkt_num, # [7] payload : frame.arr # [8] } }

    type this = struct {
        ptype : quic_packet_type, # [2]
        pversion : version, # [3]
        dst_cid : cid, # [4]
        src_cid : cid, # [5]
        token : stream_data, # [6]
        seq_num : pkt_num, # [7]
        payload : frame.arr # [8]
    }

Hamid instance retired_cids : array(idx, cid_seq) Hamid

    instance idx : unbounded_sequence
    instance arr : array(idx,this)
}


object quic_packet = {
    ...
    action long(pkt:this) returns(res:bool) = {
        res := pkt.ptype ~= quic_packet_type.one_rtt;
    }
}

Note: Short header are considered to have scid of 0 so it is quite important to use this value

Packet protocol events

The packet event

This event corresponds to transmission of a QUIC packet.

Parameters

• src: the source endpoint
• dst: the destination endpoint
• pkt : the packet contents

action packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = {}

action send_ack_eliciting_handshake_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = {}

action send_ack_eliciting_initial_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = {}

action send_ack_eliciting_application_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = {}

action packet_event_multiple_src(src1:ip.endpoint,src2:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = {}

Packet protocol state

This section defines the history variables that track the state of the packet protocol. Some of these variables are shared between protocol layers, so that the allowed interleavings of events at different layers can be specified.

Packet protocol state

• For each cid C, conn_seen(C) is true if a packet with source cid C has been transmitted.

• For each aid C, conn_closed(C) is true if C is in the closed state.

• For each aid C, conn_draining(C) is true if C is in the draining state.

• For each aid C, draining_pkt_sent(C) is true if the single packet allowed to be sent in transition to the draining state has been sent. This one packet must contain a connection_close frame with error code 0. TODO: we don't check the error code.

• For each endpoint aid C, last_pkt_num(C,L) represents the number of the latest packet sent by C in encryption level L.

• For each aid C, sent_pkt(C,L,N) is true if a packet numbered N has been sent by C in encryption level L.

• For each aid C, acked_pkt(C,L,N) is true if a packet numbered N sent by C in encryption level L has been acknowledged.

• For each aid C, max_acked(C,L) is the greatest packet number N such that acked_pkt(C,L,N), or zero if forall N. ~acked(C,L,N).

• For each aid C, ack_credit(E,C) is the number of non-ack-only packets sent to C, less the number of ack-only packets sent from C.

• For each aid C, trans_params_set(C) is true if C has declared transport parameters.

• For each aid C, function trans_params(C) gives the transport parameters declared by C.

• The predicate connected(C) indicates that the peer of aid C has been determined. This occurs conceptually when a server produces a server hello frame.

• The function connected_to(C) maps the aid C to its peer, if the peer has been determined.

• The function nonce_cid(C) maps the client aid C to the nonce cid it has chosen for its initial packet.

• The predicate is_client(C) indicates that aid 'C' is taking the client role.

• The predicate conn_requested(S,D,C) indicates that a client and endpoint S has requested to open a connection with a server at endpoint D, using cid C.

• The function hi_non_probing(C) indicates the highest packet number of a non-probing packet sent by aid C.

• The relation hi_non_probing_endpoint(C,E) that the highest-numbered non-probing packet of aid C was at some time sent from endpopint E.

• The relation pkt_has_close(C,L,N) is true if packet number N sent by aid C contained a CONNECTION_CLOSE frame.

• The relation cid_mapped(C) is true when connection ID C has been provided as new connection ID for a connection and becomes false when the C is retired

• If cid_mapped(C) is true, then the function cid_to_aid(C) gives the aid for which C is a new connection ID

• If aid D created a new connection ID with sequence number S, then seqnum_to_cid(D, S) yield the new connection id.

relation conn_seen(C:cid)
relation conn_closed(C:cid)
relation conn_draining(C:cid)
relation draining_pkt_sent(C:cid)
function last_pkt_num(C:cid,L:quic_packet_type) : pkt_num
relation sent_pkt(C:cid,L:quic_packet_type,N:pkt_num)
relation acked_pkt(C:cid,L:quic_packet_type,N:pkt_num)
function max_acked(C:cid,L:quic_packet_type) : pkt_num
function ack_credit(C:cid) : pkt_num
relation trans_params_set(C:cid)
function trans_params(C:cid) : trans_params_struct
relation connected(C:cid)
function cid_to_aid(C:cid) : cid
relation cid_mapped(C:cid)

chris

function cid_to_token(C:cid) : stream_data
function initial_token : stream_data
relation cid_mapped_token(C:cid)

chris

function seqnum_to_cid (D : cid,S : cid_seq) : cid

Hamid

function max_seq_num(C:cid) : cid_seq

Hamid

function connected_to(C:cid) : cid
function nonce_cid(C:cid) : cid
relation is_client(C:cid)
relation conn_requested(S:ip.endpoint,D:ip.endpoint,C:cid)
relation issued_zero_length_cid #(S:ip.endpoint,D:ip.endpoint) TODO pass that to handle function of frames
function hi_non_probing(C:cid) : pkt_num
relation hi_non_probing_endpoint(C:cid,E:ip.endpoint)
relation pkt_has_close(C:cid,L:quic_packet_type,N:pkt_num)

chris We start with the initial cid

function num_conn(C:cid) : stream_pos
relation tls_handshake_finished
relation migration_done

relation first_initial_send
function initial_scid : cid
function initial_dcid : cid


relation is_lost(C:cid,L:quic_packet_type,N:pkt_num)
function is_retransmitted(P:frame.arr) : pkt_num

function cid_ip_mapped(D:ip.endpoint) :cid relation cid_ip_mapped(D:ip.endpoint) chris

function dst_endpoint : ip.endpoint


relation address_validated

relation path_validated
function path_validated_pkt_num: pkt_num

function anti_amplification_limit : stream_pos

relation is_not_sleeping

Initial state

---

The history variables are initialized as follows. Initially, no connections have been seen and no packets have been sent or acknowledged.

after init {
    conn_seen(C) := false;
    last_pkt_num(C,L) := 0;
    conn_closed(C) := false;
    conn_draining(C) := false;
    draining_pkt_sent(C) := false;
    sent_pkt(C,L,N) := false;
    acked_pkt(C,L,N) := false;
    pkt_has_close(C,L,N) := false;
    max_acked(C,L) := 0;
    ack_credit(C) := 0;
    trans_params_set(C:cid) := false;
    is_client(C) := false;
    conn_requested(S,D,C) := false;
    hi_non_probing(C) := 0;
    hi_non_probing_endpoint(C,E) := false;
    cid_mapped(C) := false;

Hamid

    max_seq_num(C) := 0;

Hamid chris

    num_conn(C) := 1;
    migration_done := false;
    tls_handshake_finished := false;
    first_initial_send := false;
    issued_zero_length_cid := false;
    is_retransmitted(P) := 0;
    is_not_sleeping := true;

chris

}

Packet event specification

---

A packet event represents the transmision of a QUIC packet pkt from source endpoint src to a QUIC destination endpoint dst containing a sequence of queued frames.

Requirements

• The packet payload may not be empty [7].

• A sender may not re-use a packet number on a given connection [4].

• A packet containing only ack frames and padding is ack-only. For a given cid, the number of ack-only packets sent from src to dst must not be greater than the number of non-ack-only packets sent from dst to src [5].

• For a given connection, a server must only send packets to an address that at one time in the past sent the as packet with the highest packet numer thus far received. See notes below on migration and path challenge. [10]

• Token Length: A variable-length integer specifying the length of the Token field, in bytes. This value is zero if no token is present. Initial packets sent by the server MUST set the Token Length field to zero; clients that receive an Initial packet with a non-zero Token Length field MUST either discard the packet or generate a connection error of type PROTOCOL_VIOLATION. [11]

Upon receiving the client's Initial packet, the server can request address validation by sending a Retry packet (Section 17.2.5) containing a token. This token MUST be repeated by the client in all Initial packets it sends for that connection after it receives the Retry packet.

Effects

• The conn_seen and sent_pkt relations are updated to reflect the observed packet [1].
• The last_pkt_num function is updated to indicate the observed packets as most recent for the packet's source and cid.

Notes

• In the low-level packet encoding, the packet number may be encoded using a small number of bytes, in a way that loses information. At this layer of the protocol, however, the packets contain the original full packet number.

• On seeing a packet form a new address with the highest packect number see thus far, the server detects migration of the client. It begins sending packets to this address and initiates path validation for this address. Until path validation succeeds, the server limits data sent to the new address. Currently we cannot specify this limit because we don't know the byte size of packets or the timings of packets.

An endpoint MUST treat the following as a connection error of type TRANSPORT_PARAMETER_ERROR or PROTOCOL_VIOLATION: * absence of the retry_source_connection_id transport parameter from the server after receiving a Retry packet, [1] * presence of the retry_source_connection_id transport parameter when no Retry packet was received, or [3] * a mismatch between values received from a peer in these transport parameters and the value sent in the corresponding Destination or Source Connection ID fields of Initial packets. [2] If a zero-length connection ID is selected, the corresponding transport parameter is included with a zero-length value.

import action show_is_sleep_fake_timeout(is_sleep_fake_timeout:bool)
import action show_queued_frames(scid:cid,queued_frames:frame.arr)
import action show_current_time(t:milliseconds)

around packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) {

is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout;

    call show_current_time(time_api.c_timer.now_millis_last_bp);

call show_is_sleep_fake_timeout(is_not_sleeping); require _generating -> is_not_sleeping; require (_generating -> is_not_sleeping); require (~is_not_sleeping -> ~_generating);

    if _generating {

require ~is_not_sleeping;

    };
    if ~_generating {
        dst_endpoint := dst;
    } else {

var local_ack_delay := on_ack_sent(max_acked(dcid,e) ,e); require local_ack_delay <= local_max_ack_delay_tp;

    }

if _generating { require ~need_sent_ack_eliciting_application_packet & ~need_sent_ack_eliciting_handshake_packet & ~need_sent_ack_eliciting_initial_packet; };

    require pkt.ptype ~= quic_packet_type.zero_rtt & pkt.ptype ~= quic_packet_type.version_negociation & pkt.ptype ~= quic_packet_type.retry;

Extract the source and destination cid's and packet number from the packet.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;

    call show_num_ack_eliciting_pkt(num_ack_eliciting_pkt);
    call show_num_ack_pkt(num_ack_pkt);

call show_num_ack_eliciting_pkt(num_ack_eliciting_pkt(scid)); call show_num_ack_pkt(num_ack_pkt(scid));

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

require (~is_not_sleeping -> (num_queued_frames(scid) = 0)); # & ~_generating));

    idle_timeout(dcid) := time_api.c_timer.now_micros_last_bp;

    call show_current_idle_timeout(idle_timeout(dcid));
    call show_current_idle_timeout(idle_timeout(scid));

    is_retransmitted(pkt.payload) := is_retransmitted(pkt.payload) + 1;
    call show_is_retransmitted(seqnum_to_streampos(pkt.seq_num),is_retransmitted(pkt.payload));

    if max_idle_timeout_used > 0 {
        if idle_timeout(dcid) > max_idle_timeout_used  {
            call show_connection_timeout(idle_timeout(dcid), max_idle_timeout_used, pto_timeout*3);
            connection_timeout := true;
        }
    }

& idle_timeout > pto_timeout*3

    call show_probe_idle_timeout(pto_timeout*3);

To avoid excessively small idle timeout periods, endpoints MUST increase the idle timeout period to be at least three times the current Probe Timeout (PTO). This allows for multiple PTOs to expire, and therefore multiple probes to be sent and lost, prior to idle timeout.

    if ~_generating & connection_timeout & is_retransmitted(pkt.payload) < 2 & idle_timeout(dcid) > pto_timeout*3 {
        respect_idle_timeout := false;
        call show_connection_timeout(idle_timeout(dcid), max_idle_timeout_used, pto_timeout*3);
        call respect_idle_timeout_none;
    }

    require pkt.token.end ~= 0 -> (retry_sent(client_initial_rcid) | retry_recv(scid) | pkt.token = tls_api.upper.get_old_new_token);

    if pkt.token.end ~= 0 { #
        address_validated := true;
        anti_amplification_limit_reached := true;
    };

    if (src = client_alt | dst = client_alt) & nclients = 1 {
        migration_done := true;

call net.close(endpoint_id.client,sock); # destroy connection ?

    };

Similarly, an endpoint MUST NOT reuse a connection ID when sending to more than one destination address.

if ~_generating { if ~migration_done { cid_ip_mapped(dst) := pkt.dst_cid; } else { cid_ip_mapped(dst) := pkt.dst_cid; }; };

The destination cid must represent an existing connection, except in the case of a client initial packet, when the destination cid may be the nonce cid chosen by the client for the given source cid. TODO: The standard says that on receiving the the server's cid, the clint must switch to it. However, we can't know when that server's cid has actually been received by the client. As an example, after the server sends its first initial packet, the client might still retransmit its initial packet using the nonce cid. In some cases, we can infer that the client has in fact seen the server's cid (for example, if it packet contains an ACK frame, or a CRYPTO frame that is reponsive to a server FRAME. This is trick to check, however, and the actual servers do not seem to check it.

    require connected(dcid) |
        pkt.ptype = quic_packet_type.initial
        & is_client(scid)
        & dcid = nonce_cid(scid);

On long headers, both cids are given. If the destination cid is connected, it must be connected to the source cid (otherwise it must be a nonce generated by a client). On short headers (meaning one_rtt) the scid is not given, so we use the recorded value.

    if pkt.long {
        require connected(dcid) -> connected_to(dcid) = scid;
    } else {
        scid := connected_to(dcid);
    };

    if retry_sent(dcid) & ~_generating & ~zero_length_token & pkt.ptype = quic_packet_type.initial {
        require dcid = client_initial_rcid;
    };

The packet type must match the encryption level of the queued frames at the source.

    require pkt.ptype = queued_level(scid);

TEMPORARY: prevent big packet number jumps (work around minquic bug) Removed for MVFST that start with big PKT_NUM -> OK now

    if  _generating {

if ~is_client(scid) { #client require pkt.seq_num > last_pkt_num(scid,pkt.ptype); require pkt.seq_num <= last_pkt_num(scid,pkt.ptype) + 0x15; } else { server

        require pkt.seq_num = last_pkt_num(scid,pkt.ptype) + 0x1; # OK

}; require pkt.seq_num < last_pkt_num(scid,pkt.ptype) + 0x1 & pkt.seq_num > last_pkt_num(scid,pkt.ptype);

    };

else { # An endpoint generates an RTT sample on receiving an ACK frame that meets the following two conditions: # 1. the largest acknowledged packet number is newly acknowledged, and # 2. at least one of the newly acknowledged packets was ack-eliciting.

if queued_ack_eliciting(scid) {

}

}; last_pkt_num(scid,pkt.ptype) := pkt.seq_num;require ~sent_pkt(scid,pkt.ptype,pkt.seq_num); # [4]sent_pkt(scid,pkt.ptype,pkt.seq_num) := true; # [1] The payload may not be empty require num_queued_frames(scid) > 0; # [7] The payload must exactly match the queued frames. if _generating {if packets_to_retransmit_end(pkt.ptype) > 0 {var paylo := packets_to_retransmit(pkt.ptype,packets_to_retransmit_end(pkt.ptype));# TODO change and put that at frame levelrequire pkt.payload = paylo;packets_to_retransmit_end(pkt.ptype) := packets_to_retransmit_end(pkt.ptype) - 1;call show_retransmit_lost_packet(paylo);}else {require pkt.payload = queued_frames(scid);};}else {call show_queued_frames(scid,queued_frames(scid));call is_generating(_generating);call show_pkt_num(pkt.seq_num);require pkt.payload = queued_frames(scid);}; TEMPORARY: don't allow client migration during handshake

    require conn_seen(scid) & pkt.long & is_client(scid) -> conn_requested(src,dst,scid);

Packet must be sent to the endpoint from which the highest numbered packet has been received. ~queued_challenge(dcid) & call show_probing(dcid ,hi_non_probing(dcid));

    require  conn_seen(dcid) -> hi_non_probing_endpoint(dcid,dst);  # [10]

TEMPORARY: do not apply ack-only rule to generated packets This can be removed when we have a frame queue per encryption level

    call show_ack_credit(scid, ack_credit(scid), queued_ack_eliciting(scid), queued_non_ack(scid), pkt.seq_num);
    require ~_generating & ~queued_non_ack(scid) -> ack_credit(scid) > 0;  # [5]

Hamid - This is wrong, because if there is no ack credits, it prevents from sending a packet containing only a CONNECTION_CLOSE frame but we want to stop packets that contain only ACKs require ~_generating & ~queued_ack_eliciting(scid) -> ack_credit(scid) > 0; Hamid

Question

THis sentence is from draft-18 section 13.1: "An endpoint MUST NOT send a packet containing only an ACK frame in response to a packet containing only ACK or PADDING frames, even if there are packet gaps which precede the received packet." Do we interpret this to mean that an ack-only packet cannot ack only ack-only packets? Or that an ack-only packet cannot ack any ack-only packets?

If the sender is in the draining state, this is the draining packet. Make sure that a draining packet has not previously been sent and that the packet contains a connection_close frame;

    if conn_draining(scid) {
        require ~draining_pkt_sent(scid) & queued_close(scid);
    };

    ...

Here, we have the updates to the packet protocol state.

Temporary

The following are repeated because currently locals defined in the "before" section cannot be accessed in the "after" section.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid if pkt.long else connected_to(dcid);

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

TODO: the following should not be here

    if pkt.ptype = quic_packet_type.initial {
        initial_token := pkt.token;

An initial packet with an unseen destination cid is a connection request.

        if ~conn_seen(dcid)  {
            if ~zero_rtt_sent {
                call show_initial_request_initial;
                call tls_client_initial_request(src,dst,dcid,pkt.pversion,src_tls_id(src));
            };
            conn_requested(src,dst,scid) := true;
        };
        cid_to_token(dcid) := pkt.token;
    };

    conn_seen(scid) := true;  # [1]

Update the ack credits. A non-ack packet sent to a destination increases the destination's ack credit. An ack packet decreases the sender's ack credit.

Hamid

if queued_non_ack(scid) { ack_credit(dcid) := ack_credit(dcid) + 1; } else { ack_credit(scid) := ack_credit(scid) - 1; };

    if queued_ack_eliciting(scid) {
        if _generating {
            num_ack_eliciting_pkt := num_ack_eliciting_pkt + 1;
        }
        ack_eliciting_threshold_current_val(dcid) := ack_eliciting_threshold_current_val(dcid) + 1;
        ack_credit(dcid) := ack_credit(dcid) + 1;
    } else {
        if ~_generating {
            num_ack_pkt:= num_ack_pkt + 1;
        }
    };
    if ~queued_non_ack(scid) {
       ack_credit(scid) := ack_credit(scid) - 1;
    };

Hamid

If this is a non-probing packet, update the highest non-probing packet number seen on from this aid. QUESTION: what if two different paths send the same packet number? QUESTION: how do you compare packet numbers with different encryption levels?

    if queued_non_probing(scid) {
        if pkt.ptype = quic_packet_type.one_rtt {
            if pkt.seq_num >= hi_non_probing(scid) {
                hi_non_probing(scid) := pkt.seq_num;
                hi_non_probing_endpoint(scid,src) := true;
            }
        } else {
            hi_non_probing_endpoint(scid,src) := true;
        }
    };

If the packet contains a close frame, then set pkt_has_close

    if queued_close(scid) {
        pkt_has_close(scid,pkt.ptype,pkt.seq_num) := true;
    };

If the sender is in the draining state, this is the draining packet.

    if conn_draining(scid) {
        draining_pkt_sent(scid) := true
    };

    if pkt.ptype = quic_packet_type.initial & ~first_initial_send & zero_rtt_allowed {
        first_initial_send := true;
        initial_scid := scid;
        initial_dcid := dcid;
        queued_level(the_cid) := quic_packet_type.zero_rtt; # todo multiple client
    } else {
        first_initial_send := false;
    };

The queued frames are deleted

    queued_frames(scid) := frame.arr.empty;
    queued_non_probing(scid) := false;
    queued_non_ack(scid) := false;
    queued_close(scid) := false;
    num_queued_frames(scid) := 0;

Hamid

    queued_ack_eliciting(scid) := false;

Hamid

}

import action show_retransmit_lost_packet(paylo:frame.arr)

import action show_connection_timeout(idle_timeout:microseconds, max_idle_timeout_used:microseconds, pto_timeout:microseconds)

around send_ack_eliciting_handshake_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) {

is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout; require _generating -> is_not_sleeping; require (_generating -> is_not_sleeping); require (~is_not_sleeping -> ~_generating);

    require pkt.ptype = quic_packet_type.handshake;
    require need_sent_ack_eliciting_handshake_packet;

Extract the source and destination cid's and packet number from the packet.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;
    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

    require pkt.ptype = queued_level(scid);

    require pkt.token.end ~= 0 -> (retry_sent(client_initial_rcid) | retry_recv(scid) | pkt.token = tls_api.upper.get_old_new_token);

    if (src = client_alt | dst = client_alt) & nclients = 1 {
        migration_done := true;
    };

Similarly, an endpoint MUST NOT reuse a connection ID when sending to more than one destination address.

The destination cid must represent an existing connection, except in the case of a client initial packet, when the destination cid may be the nonce cid chosen by the client for the given source cid. TODO: The standard says that on receiving the the server's cid, the clint must switch to it. However, we can't know when that server's cid has actually been received by the client. As an example, after the server sends its first initial packet, the client might still retransmit its initial packet using the nonce cid. In some cases, we can infer that the client has in fact seen the server's cid (for example, if it packet contains an ACK frame, or a CRYPTO frame that is reponsive to a server FRAME. This is trick to check, however, and the actual servers do not seem to check it.

    require connected(dcid) |
        pkt.ptype = quic_packet_type.initial
        & is_client(scid)
        & dcid = nonce_cid(scid);

On long headers, both cids are given. If the destination cid is connected, it must be connected to the source cid (otherwise it must be a nonce generated by a client). On short headers (meaning one_rtt) the scid is not given, so we use the recorded value.

    if pkt.long {
        require connected(dcid) -> connected_to(dcid) = scid;
    } else {
        scid := connected_to(dcid);
    };

    if retry_sent(dcid) & ~_generating & ~zero_length_token & pkt.ptype = quic_packet_type.initial {
        require dcid = client_initial_rcid;
    };

TEMPORARY: prevent big packet number jumps (work around minquic bug) Removed for MVFST that start with big PKT_NUM -> OK now

    if  _generating {

if ~is_client(scid) { #client require pkt.seq_num > last_pkt_num(scid,pkt.ptype); require pkt.seq_num <= last_pkt_num(scid,pkt.ptype) + 0x15; } else { server

        require pkt.seq_num = last_pkt_num(scid,pkt.ptype) + 0x1; # OK

}; require pkt.seq_num < last_pkt_num(scid,pkt.ptype) + 0x1 & pkt.seq_num > last_pkt_num(scid,pkt.ptype);

    };

else { # An endpoint generates an RTT sample on receiving an ACK frame that meets the following two conditions: # 1. the largest acknowledged packet number is newly acknowledged, and # 2. at least one of the newly acknowledged packets was ack-eliciting.

if queued_ack_eliciting(scid) {

}

}; last_pkt_num(scid,pkt.ptype) := pkt.seq_num;require ~sent_pkt(scid,pkt.ptype,pkt.seq_num); # [4]sent_pkt(scid,pkt.ptype,pkt.seq_num) := true; # [1] The payload may not be empty

    require num_queued_frames(scid) > 0;  # [7]

The payload must exactly match the queued frames.

    require pkt.payload = queued_frames(scid);

TEMPORARY: don't allow client migration during handshake

    require conn_seen(scid) & pkt.long & is_client(scid) -> conn_requested(src,dst,scid);

Packet must be sent to the endpoint from which the highest numbered packet has been received. ~queued_challenge(dcid) & call show_probing(dcid ,hi_non_probing(dcid));

    require  conn_seen(dcid) -> hi_non_probing_endpoint(dcid,dst);  # [10]

TEMPORARY: do not apply ack-only rule to generated packets This can be removed when we have a frame queue per encryption level

call show_ack_credit(scid, ack_credit(scid), queued_ack_eliciting(scid), queued_non_ack(scid), pkt.seq_num);

    require ~_generating & ~queued_non_ack(scid) -> ack_credit(scid) > 0;  # [5]

Hamid - This is wrong, because if there is no ack credits, it prevents from sending a packet containing only a CONNECTION_CLOSE frame but we want to stop packets that contain only ACKs require ~_generating & ~queued_ack_eliciting(scid) -> ack_credit(scid) > 0; Hamid

Question

THis sentence is from draft-18 section 13.1: "An endpoint MUST NOT send a packet containing only an ACK frame in response to a packet containing only ACK or PADDING frames, even if there are packet gaps which precede the received packet." Do we interpret this to mean that an ack-only packet cannot ack only ack-only packets? Or that an ack-only packet cannot ack any ack-only packets?

If the sender is in the draining state, this is the draining packet. Make sure that a draining packet has not previously been sent and that the packet contains a connection_close frame;

    if conn_draining(scid) {
        require ~draining_pkt_sent(scid) & queued_close(scid);
    };

    ...

Here, we have the updates to the packet protocol state.

Temporary

The following are repeated because currently locals defined in the "before" section cannot be accessed in the "after" section.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid if pkt.long else connected_to(dcid);

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

if is

Todo

the following should not be here

    if pkt.ptype = quic_packet_type.initial {
        initial_token := pkt.token;

An initial packet with an unseen destination cid is a connection request.

        if ~conn_seen(dcid)  {
            if ~zero_rtt_sent {
                call show_initial_request_initial;
                call tls_client_initial_request(src,dst,dcid,pkt.pversion,src_tls_id(src));
            };
            conn_requested(src,dst,scid) := true;
        };
        cid_to_token(dcid) := pkt.token;
    };

    conn_seen(scid) := true;  # [1]

Update the ack credits. A non-ack packet sent to a destination increases the destination's ack credit. An ack packet decreases the sender's ack credit.

Hamid

if queued_non_ack(scid) { ack_credit(dcid) := ack_credit(dcid) + 1; } else { ack_credit(scid) := ack_credit(scid) - 1; };

    if queued_ack_eliciting(scid) {
       ack_credit(dcid) := ack_credit(dcid) + 1;
    };
    if ~queued_non_ack(scid) {
       ack_credit(scid) := ack_credit(scid) - 1;
    };

Hamid

If this is a non-probing packet, update the highest non-probing packet number seen on from this aid. QUESTION: what if two different paths send the same packet number? QUESTION: how do you compare packet numbers with different encryption levels?

    if queued_non_probing(scid) {
        if pkt.ptype = quic_packet_type.one_rtt {
            if pkt.seq_num >= hi_non_probing(scid) {
                hi_non_probing(scid) := pkt.seq_num;
                hi_non_probing_endpoint(scid,src) := true;
            }
        } else {
            hi_non_probing_endpoint(scid,src) := true;
        }
    };

If the packet contains a close frame, then set pkt_has_close

    if queued_close(scid) {
        pkt_has_close(scid,pkt.ptype,pkt.seq_num) := true;
    };

If the sender is in the draining state, this is the draining packet.

    if conn_draining(scid) {
        draining_pkt_sent(scid) := true
    };

    if pkt.ptype = quic_packet_type.initial & ~first_initial_send & zero_rtt_allowed {
        first_initial_send := true;
        initial_scid := scid;
        initial_dcid := dcid;
        queued_level(the_cid) := quic_packet_type.zero_rtt; # todo multiple client
    } else {
        first_initial_send := false;
    };

The queued frames are deleted

    queued_frames(scid) := frame.arr.empty;
    queued_non_probing(scid) := false;
    queued_non_ack(scid) := false;
    queued_close(scid) := false;
    num_queued_frames(scid) := 0;

Hamid

    queued_ack_eliciting(scid) := false;

Hamid

    need_sent_ack_eliciting_handshake_packet := false
}

around send_ack_eliciting_application_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) {

is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout; require _generating -> is_not_sleeping; require (_generating -> is_not_sleeping); require (~is_not_sleeping -> ~_generating);

    if _generating {

    };
    require pkt.ptype = quic_packet_type.one_rtt;
    require need_sent_ack_eliciting_application_packet;

Extract the source and destination cid's and packet number from the packet.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;
    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

    require pkt.ptype = queued_level(scid);

require pkt.token.end ~= 0 -> (retry_sent(client_initial_rcid) | retry_recv(scid) | pkt.token = tls_api.upper.get_old_new_token);

    require pkt.token.end = 0;
    if (src = client_alt | dst = client_alt) & nclients = 1 {
        migration_done := true;
    };

Similarly, an endpoint MUST NOT reuse a connection ID when sending to more than one destination address.

The destination cid must represent an existing connection, except in the case of a client initial packet, when the destination cid may be the nonce cid chosen by the client for the given source cid. TODO: The standard says that on receiving the the server's cid, the clint must switch to it. However, we can't know when that server's cid has actually been received by the client. As an example, after the server sends its first initial packet, the client might still retransmit its initial packet using the nonce cid. In some cases, we can infer that the client has in fact seen the server's cid (for example, if it packet contains an ACK frame, or a CRYPTO frame that is reponsive to a server FRAME. This is trick to check, however, and the actual servers do not seem to check it.

    require connected(dcid) |
        pkt.ptype = quic_packet_type.initial
        & is_client(scid)
        & dcid = nonce_cid(scid);

On long headers, both cids are given. If the destination cid is connected, it must be connected to the source cid (otherwise it must be a nonce generated by a client). On short headers (meaning one_rtt) the scid is not given, so we use the recorded value.

    if pkt.long {
        require connected(dcid) -> connected_to(dcid) = scid;
    } else {
        scid := connected_to(dcid);
    };

    if retry_sent(dcid) & ~_generating & ~zero_length_token & pkt.ptype = quic_packet_type.initial {
        require dcid = client_initial_rcid;
    };

TEMPORARY: prevent big packet number jumps (work around minquic bug) Removed for MVFST that start with big PKT_NUM -> OK now

    if  _generating {

if ~is_client(scid) { #client require pkt.seq_num > last_pkt_num(scid,pkt.ptype); require pkt.seq_num <= last_pkt_num(scid,pkt.ptype) + 0x15; } else { server

        require pkt.seq_num = last_pkt_num(scid,pkt.ptype) + 0x1; # OK

}; require pkt.seq_num < last_pkt_num(scid,pkt.ptype) + 0x1 & pkt.seq_num > last_pkt_num(scid,pkt.ptype);

    };

else { # An endpoint generates an RTT sample on receiving an ACK frame that meets the following two conditions: # 1. the largest acknowledged packet number is newly acknowledged, and # 2. at least one of the newly acknowledged packets was ack-eliciting.

if queued_ack_eliciting(scid) {

}

}; last_pkt_num(scid,pkt.ptype) := pkt.seq_num;require ~sent_pkt(scid,pkt.ptype,pkt.seq_num); # [4]sent_pkt(scid,pkt.ptype,pkt.seq_num) := true; # [1] The payload may not be empty

    require num_queued_frames(scid) > 0;  # [7]

The payload must exactly match the queued frames.

    require pkt.payload = queued_frames(scid);

TEMPORARY: don't allow client migration during handshake

    require conn_seen(scid) & pkt.long & is_client(scid) -> conn_requested(src,dst,scid);

Packet must be sent to the endpoint from which the highest numbered packet has been received. ~queued_challenge(dcid) & call show_probing(dcid ,hi_non_probing(dcid));

    require  conn_seen(dcid) -> hi_non_probing_endpoint(dcid,dst);  # [10]

TEMPORARY: do not apply ack-only rule to generated packets This can be removed when we have a frame queue per encryption level

call show_ack_credit(scid, ack_credit(scid), queued_ack_eliciting(scid), queued_non_ack(scid), pkt.seq_num);

    require ~_generating & ~queued_non_ack(scid) -> ack_credit(scid) > 0;  # [5]

Hamid - This is wrong, because if there is no ack credits, it prevents from sending a packet containing only a CONNECTION_CLOSE frame but we want to stop packets that contain only ACKs require ~_generating & ~queued_ack_eliciting(scid) -> ack_credit(scid) > 0; Hamid

Question

THis sentence is from draft-18 section 13.1: "An endpoint MUST NOT send a packet containing only an ACK frame in response to a packet containing only ACK or PADDING frames, even if there are packet gaps which precede the received packet." Do we interpret this to mean that an ack-only packet cannot ack only ack-only packets? Or that an ack-only packet cannot ack any ack-only packets?

If the sender is in the draining state, this is the draining packet. Make sure that a draining packet has not previously been sent and that the packet contains a connection_close frame;

    if conn_draining(scid) {
        require ~draining_pkt_sent(scid) & queued_close(scid);
    };

    ...

Here, we have the updates to the packet protocol state.

Temporary

The following are repeated because currently locals defined in the "before" section cannot be accessed in the "after" section.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid if pkt.long else connected_to(dcid);

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

if is

Todo

the following should not be here

    if pkt.ptype = quic_packet_type.initial {
        initial_token := pkt.token;

An initial packet with an unseen destination cid is a connection request.

        if ~conn_seen(dcid)  {
            if ~zero_rtt_sent {
                call show_initial_request_initial;
                call tls_client_initial_request(src,dst,dcid,pkt.pversion,src_tls_id(src));
            };
            conn_requested(src,dst,scid) := true;
        };
        cid_to_token(dcid) := pkt.token;
    };

    conn_seen(scid) := true;  # [1]

Update the ack credits. A non-ack packet sent to a destination increases the destination's ack credit. An ack packet decreases the sender's ack credit.

Hamid

if queued_non_ack(scid) { ack_credit(dcid) := ack_credit(dcid) + 1; } else { ack_credit(scid) := ack_credit(scid) - 1; };

    if queued_ack_eliciting(scid) {

num_ack_eliciting_pkt(scid) := num_ack_eliciting_pkt(scid) + 1;

        ack_credit(dcid) := ack_credit(dcid) + 1;
    } else {

num_ack_pkt(scid) := num_ack_pkt(scid) + 1;

    };
    if ~queued_non_ack(scid) {
       ack_credit(scid) := ack_credit(scid) - 1;
    };

Hamid

If this is a non-probing packet, update the highest non-probing packet number seen on from this aid. QUESTION: what if two different paths send the same packet number? QUESTION: how do you compare packet numbers with different encryption levels?

    if queued_non_probing(scid) {
        if pkt.ptype = quic_packet_type.one_rtt {
            if pkt.seq_num >= hi_non_probing(scid) {
                hi_non_probing(scid) := pkt.seq_num;
                hi_non_probing_endpoint(scid,src) := true;
            }
        } else {
            hi_non_probing_endpoint(scid,src) := true;
        }
    };

If the packet contains a close frame, then set pkt_has_close

    if queued_close(scid) {
        pkt_has_close(scid,pkt.ptype,pkt.seq_num) := true;
    };

If the sender is in the draining state, this is the draining packet.

    if conn_draining(scid) {
        draining_pkt_sent(scid) := true
    };

    if pkt.ptype = quic_packet_type.initial & ~first_initial_send & zero_rtt_allowed {
        first_initial_send := true;
        initial_scid := scid;
        initial_dcid := dcid;
        queued_level(the_cid) := quic_packet_type.zero_rtt; # todo multiple client
    } else {
        first_initial_send := false;
    };

The queued frames are deleted

    queued_frames(scid) := frame.arr.empty;
    queued_non_probing(scid) := false;
    queued_non_ack(scid) := false;
    queued_close(scid) := false;
    num_queued_frames(scid) := 0;

Hamid

    queued_ack_eliciting(scid) := false;

Hamid

    need_sent_ack_eliciting_application_packet := false
}


around send_ack_eliciting_initial_packet(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) {

is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout; require _generating -> is_not_sleeping; require (_generating -> is_not_sleeping); if _generating {

}; require (~is_not_sleeping -> ~_generating);

    require pkt.ptype = quic_packet_type.initial;

    require need_sent_ack_eliciting_initial_packet;

Extract the source and destination cid's and packet number from the packet.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;
    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };


    require pkt.ptype = queued_level(scid);


    require pkt.token.end ~= 0 -> (retry_sent(client_initial_rcid) | retry_recv(scid) | pkt.token = tls_api.upper.get_old_new_token);

    if (src = client_alt | dst = client_alt) & nclients = 1 {
        migration_done := true;
    };

Similarly, an endpoint MUST NOT reuse a connection ID when sending to more than one destination address.

The destination cid must represent an existing connection, except in the case of a client initial packet, when the destination cid may be the nonce cid chosen by the client for the given source cid. TODO: The standard says that on receiving the the server's cid, the clint must switch to it. However, we can't know when that server's cid has actually been received by the client. As an example, after the server sends its first initial packet, the client might still retransmit its initial packet using the nonce cid. In some cases, we can infer that the client has in fact seen the server's cid (for example, if it packet contains an ACK frame, or a CRYPTO frame that is reponsive to a server FRAME. This is trick to check, however, and the actual servers do not seem to check it.

    require connected(dcid) |
        pkt.ptype = quic_packet_type.initial
        & is_client(scid)
        & dcid = nonce_cid(scid);

On long headers, both cids are given. If the destination cid is connected, it must be connected to the source cid (otherwise it must be a nonce generated by a client). On short headers (meaning one_rtt) the scid is not given, so we use the recorded value.

    if pkt.long {
        require connected(dcid) -> connected_to(dcid) = scid;
    } else {
        scid := connected_to(dcid);
    };

    if retry_sent(dcid) & ~_generating & ~zero_length_token & pkt.ptype = quic_packet_type.initial {
        require dcid = client_initial_rcid;
    };

TEMPORARY: prevent big packet number jumps (work around minquic bug) Removed for MVFST that start with big PKT_NUM -> OK now if _generating { if ~is_client(scid) { #client require pkt.seq_num > last_pkt_num(scid,pkt.ptype); require pkt.seq_num <= last_pkt_num(scid,pkt.ptype) + 0x15; } else { server

        require pkt.seq_num = last_pkt_num(scid,pkt.ptype) + 0x15; # OK

}; require pkt.seq_num < last_pkt_num(scid,pkt.ptype) + 0x1 & pkt.seq_num > last_pkt_num(scid,pkt.ptype); }; else { # An endpoint generates an RTT sample on receiving an ACK frame that meets the following two conditions: # 1. the largest acknowledged packet number is newly acknowledged, and # 2. at least one of the newly acknowledged packets was ack-eliciting.

if queued_ack_eliciting(scid) {

}

}; last_pkt_num(scid,pkt.ptype) := pkt.seq_num;require ~sent_pkt(scid,pkt.ptype,pkt.seq_num); # [4]sent_pkt(scid,pkt.ptype,pkt.seq_num) := true; # [1] The payload may not be empty

    require num_queued_frames(scid) > 0;  # [7]

The payload must exactly match the queued frames.

    require pkt.payload = queued_frames(scid);

TEMPORARY: don't allow client migration during handshake

    require conn_seen(scid) & pkt.long & is_client(scid) -> conn_requested(src,dst,scid);

Packet must be sent to the endpoint from which the highest numbered packet has been received. ~queued_challenge(dcid) & call show_probing(dcid ,hi_non_probing(dcid));

    require  conn_seen(dcid) -> hi_non_probing_endpoint(dcid,dst);  # [10]

TEMPORARY: do not apply ack-only rule to generated packets This can be removed when we have a frame queue per encryption level

call show_ack_credit(scid, ack_credit(scid), queued_ack_eliciting(scid), queued_non_ack(scid), pkt.seq_num);

    require ~_generating & ~queued_non_ack(scid) -> ack_credit(scid) > 0;  # [5]

Hamid - This is wrong, because if there is no ack credits, it prevents from sending a packet containing only a CONNECTION_CLOSE frame but we want to stop packets that contain only ACKs require ~_generating & ~queued_ack_eliciting(scid) -> ack_credit(scid) > 0; Hamid

Question

THis sentence is from draft-18 section 13.1: "An endpoint MUST NOT send a packet containing only an ACK frame in response to a packet containing only ACK or PADDING frames, even if there are packet gaps which precede the received packet." Do we interpret this to mean that an ack-only packet cannot ack only ack-only packets? Or that an ack-only packet cannot ack any ack-only packets?

If the sender is in the draining state, this is the draining packet. Make sure that a draining packet has not previously been sent and that the packet contains a connection_close frame;

    if conn_draining(scid) {
        require ~draining_pkt_sent(scid) & queued_close(scid);
    };

    ...

Here, we have the updates to the packet protocol state.

Temporary

The following are repeated because currently locals defined in the "before" section cannot be accessed in the "after" section.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid if pkt.long else connected_to(dcid);

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

if is

Todo

the following should not be here

    if pkt.ptype = quic_packet_type.initial {
        initial_token := pkt.token;

An initial packet with an unseen destination cid is a connection request.

        if ~conn_seen(dcid)  {
            if ~zero_rtt_sent {
                call show_initial_request_initial;
                call tls_client_initial_request(src,dst,dcid,pkt.pversion,src_tls_id(src));
            };
            conn_requested(src,dst,scid) := true;
        };
        cid_to_token(dcid) := pkt.token;
    };

    conn_seen(scid) := true;  # [1]

Update the ack credits. A non-ack packet sent to a destination increases the destination's ack credit. An ack packet decreases the sender's ack credit.

Hamid

if queued_non_ack(scid) { ack_credit(dcid) := ack_credit(dcid) + 1; } else { ack_credit(scid) := ack_credit(scid) - 1; };

    if queued_ack_eliciting(scid) {
       ack_credit(dcid) := ack_credit(dcid) + 1;
    };
    if ~queued_non_ack(scid) {
       ack_credit(scid) := ack_credit(scid) - 1;
    };

Hamid

If this is a non-probing packet, update the highest non-probing packet number seen on from this aid. QUESTION: what if two different paths send the same packet number? QUESTION: how do you compare packet numbers with different encryption levels?

    if queued_non_probing(scid) {
        if pkt.ptype = quic_packet_type.one_rtt {
            if pkt.seq_num >= hi_non_probing(scid) {
                hi_non_probing(scid) := pkt.seq_num;
                hi_non_probing_endpoint(scid,src) := true;
            }
        } else {
            hi_non_probing_endpoint(scid,src) := true;
        }
    };

If the packet contains a close frame, then set pkt_has_close

    if queued_close(scid) {
        pkt_has_close(scid,pkt.ptype,pkt.seq_num) := true;
    };

If the sender is in the draining state, this is the draining packet.

    if conn_draining(scid) {
        draining_pkt_sent(scid) := true
    };

    if pkt.ptype = quic_packet_type.initial & ~first_initial_send & zero_rtt_allowed {
        first_initial_send := true;
        initial_scid := scid;
        initial_dcid := dcid;
        queued_level(the_cid) := quic_packet_type.zero_rtt; # todo multiple client
    } else {
        first_initial_send := false;
    };

The queued frames are deleted

    queued_frames(scid) := frame.arr.empty;
    queued_non_probing(scid) := false;
    queued_non_ack(scid) := false;
    queued_close(scid) := false;
    num_queued_frames(scid) := 0;

Hamid

    queued_ack_eliciting(scid) := false;

Hamid

    need_sent_ack_eliciting_initial_packet := false;
}


import action show_initial_request_initial
import action show_is_retransmitted(p:stream_pos, c_time:pkt_num)
import action respect_idle_timeout_none

Procedures ==========

TLS extensions are used in the client hello and server hello messages to carry the QUIC transport parameters, via special TLS extension type quic_transport_parameters. This type is defined in the reference quic_transport_parameters. Here we have procedures that infer the transport parameters events from the TLS handshake messages that transmit the parameters.

Todo

This inference is not really needed. It should be possible to obtain the parameters directly from the TLS API. We infer the parameters here only for historical reasons.

The handle_tls_handshake rules apply to each client_hello, server_hello or encrypted extensions message, in order of occurrence in the crypto data. The last parameter, is_client_hello, is true for a client_hello message (see below).

action handle_tls_handshake(src:ip.endpoint, dst:ip.endpoint, scid:cid, dcid:cid,hs:tls.handshake) = {
    if some(ch:tls.client_hello) hs *> ch {
        is_client(scid) := true;
        call handle_tls_extensions(src,dst,scid,ch.extensions,true);
    }
    else if some(sh:tls.server_hello) hs *> sh {

call map_cids(src,scid,dcid); # [1] call map_cids(dst,dcid,scid);

        call handle_tls_extensions(src,dst,scid,sh.extensions,false);
    }
    else if some(ee:tls.encrypted_extensions) hs *> ee {
        call handle_tls_extensions(src,dst,scid,ee.extensions,false);
    }
    if some(fh:tls.finished) hs *> fh {
        tls_handshake_finished := true;
    }
}

The rules in handle_client_transport_parameters apply to each quic_transport_parameters extension instance in order of occurrence.

action handle_tls_extensions(src:ip.endpoint,dst:ip.endpoint, scid:cid, exts:vector[tls.extension], is_client_hello:bool) = {

We process the extensions in a message in order.

    var idx := exts.begin;
    while idx < exts.end {
        var ext := exts.value(idx);

For every quic_transport_parameters extension...

        if some (tps:quic_transport_parameters) ext *> tps {
            call handle_client_transport_parameters(src,dst,scid,tps,is_client_hello);
            trans_params_set(scid) := true;
        };
        idx := idx.next
    };
}

The rules in handle_transport_parameter apply to each transport_parameter instance a quic_transport_parameters extension, in order of occurrence.

Requirements:

• The endpoint must issue an initial_max_stream_data value [1]. [not anymore]
• The endpoint must issue an initial_max_data value [2].
• The endpoint must issue an max_idle_timeout value [3]. [not anymore chris]
• A client must not issue an stateless_reset_token value [4].
• The endpoint must issue an initial_source_connection_id value [5]. [chris]
• A server must issue an original_destination_connection_id value [6].

An endpoint's min_ack_delay MUST NOT be greater than the its max_ack_delay. Endpoints that support this extension MUST treat receipt of a min_ack_delay that is greater than the received max_ack_delay as a connection error of type TRANSPORT_PARAMETER_ERROR. [7] Note that while the endpoint's max_ack_delay transport parameter is in milliseconds (Section 18.2 of [QUIC-TRANSPORT]), min_ack_delay is specified in microseconds. An endpoint MUST treat the following as a connection error of type TRANSPORT_PARAMETER_ERROR or PROTOCOL_VIOLATION: * absence of the retry_source_connection_id transport parameter from the server after receiving a Retry packet, Note:

• Setting a transport parameter requires that the parameter is not previously set.

action handle_client_transport_parameters(src:ip.endpoint,dst:ip.endpoint,scid:cid, tps:quic_transport_parameters, is_client_hello : bool) = {

call client_transport_parameters_event(src,dst,scid,tps);

    var idx := tps.transport_parameters.begin;
    while idx < tps.transport_parameters.end {
        trans_params(scid) := tps.transport_parameters.value(idx).set(trans_params(scid));
        idx := idx.next
    };

require initial_max_stream_data_bidi_local.is_set(trans_params(scid)); # [1] require initial_max_data.is_set(trans_params(scid)); # [2] require max_idle_timeout.is_set(trans_params(scid)); # [3] TODO require initial_max_stream_data_bidi_remote.is_set(trans_params(scid)); # [1] require initial_max_stream_data_uni.is_set(trans_params(scid)); # [1]

    if ~ _generating  {

for tests where we check that the implementation behave well if not present

        if client_non_zero_scil & ~(scid = 1) & (client_initial_version = 0x00000001 | client_initial_version = 0x00000001){ # TODO
            require initial_source_connection_id.is_set(trans_params(scid));  # [5]
        };
    };
    if is_client_hello {
        require ~stateless_reset_token.is_set(trans_params(scid));  # [4]
    } else {
        if ~ _generating & ~(scid = 1) {  # TODO
            require original_destination_connection_id.is_set(trans_params(scid));  # [6]
        };
    };

    if ~is_client_hello & (retry_recv(client_initial_rcid) | retry_sent(client_initial_rcid)) & ~zero_length_token {
        require retry_source_connection_id.is_set(trans_params(scid));
        require retry_source_connection_id.value(trans_params(scid)).rcid = client_initial_rcid; # todo generalize
    };

    if max_ack_delay.is_set(trans_params(scid)) {
        max_ack_delay_tp := milliseconds_to_microseconds(max_ack_delay.value(trans_params(scid)).exponent_8);
        call show_max_ack_delay(max_ack_delay_tp);
    }

    if ack_delay_exponent.is_set(trans_params(scid)) {
        require ack_delay_exponent.value(trans_params(scid)).exponent_8 <= 20;
        ack_delay_exponent_tp := ack_delay_exponent.value(trans_params(scid)).exponent_8;
        call show_ack_delay_exponent(ack_delay_exponent_tp);
    }

[7]

    if min_ack_delay.is_set(trans_params(scid)) & max_ack_delay.is_set(trans_params(scid)) {
        var min_ack_milli := min_ack_delay.value(trans_params(scid)).exponent_8; #  * 1000;
        require  min_ack_milli < milliseconds_to_microseconds(max_ack_delay.value(trans_params(scid)).exponent_8);  # [1]
    };

Chris If a max_idle_timeout is specified by either endpoint in its transport parameters (Section 18.2), the connection is silently closed and its state is discarded when it remains idle for longer than the minimum of the max_idle_timeout value advertised by both endpoints. -> An endpoint that sends packets close to the effective timeout risks having them be discarded at the peer, since the idle timeout period might have expired at the peer before these packets arrive.

    if max_idle_timeout.is_set(trans_params(scid)) {
        if is_client_hello {
            max_idle_timeout_client := milliseconds_to_microseconds(max_idle_timeout.value(trans_params(scid)).seconds_16)
        } else {
            max_idle_timeout_server := milliseconds_to_microseconds(max_idle_timeout.value(trans_params(scid)).seconds_16)
        }
        if max_idle_timeout_client = 0 {
            max_idle_timeout_used := max_idle_timeout_server;
        } else if max_idle_timeout_server = 0 {
            max_idle_timeout_used := max_idle_timeout_client;
        } else if max_idle_timeout_server < max_idle_timeout_client {
            max_idle_timeout_used := max_idle_timeout_server;
        } else {
            max_idle_timeout_used := max_idle_timeout_client;
        }
        call max_idle_timeout_update(max_idle_timeout_used);
    }

var initial_max_stream_data_uni_server_0rtt : stream_pos_32; var initial_max_stream_data_bidi_remote_server_0rtt : stream_pos_32; var initial_max_data_server_0rtt : stream_pos_32; var initial_max_stream_data_bidi_local_server_0rtt : stream_pos_32; var initial_max_stream_id_bidi_server_0rtt : stream_pos_32; var active_connection_id_limit_server_0rtt : stream_pos_32; [6-0rtt]

    if zero_rtt_server_test & ~is_client_hello {
        if initial_max_stream_data_uni.is_set(trans_params(scid)) {
            require initial_max_stream_data_uni.value(trans_params(scid)).stream_pos_32 >= initial_max_stream_data_uni_server_0rtt; # todo generalize
        };
        if initial_max_stream_data_bidi_remote.is_set(trans_params(scid)) {
            require initial_max_stream_data_bidi_remote.value(trans_params(scid)).stream_pos_32 >= initial_max_stream_data_bidi_remote_server_0rtt; # todo generalize
        };
        if initial_max_data.is_set(trans_params(scid)) {
            require initial_max_data.value(trans_params(scid)).stream_pos_32 >= initial_max_data_server_0rtt; # todo generalize
        };
        if initial_max_stream_data_bidi_local.is_set(trans_params(scid)) {
            require initial_max_stream_data_bidi_local.value(trans_params(scid)).stream_pos_32 >= initial_max_stream_data_bidi_local_server_0rtt; # todo generalize
        };
        if initial_max_stream_id_bidi.is_set(trans_params(scid)) {
            require initial_max_stream_id_bidi.value(trans_params(scid)).stream_id_16 >= initial_max_stream_id_bidi_server_0rtt; # todo generalize
        };
        if active_connection_id_limit.is_set(trans_params(scid)) {
            require active_connection_id_limit.value(trans_params(scid)).stream_pos_32 >= active_connection_id_limit_server_0rtt; # todo generalize
        };
    };

save server TPs

    if ~is_client_hello {
        if initial_max_stream_data_uni.is_set(trans_params(scid)) {
            call tls_api.upper.save_initial_max_stream_data_uni(initial_max_stream_data_uni.value(trans_params(scid)).stream_pos_32);
        };
        if initial_max_stream_data_bidi_remote.is_set(trans_params(scid)) {
            call tls_api.upper.save_initial_max_stream_data_bidi_remote(initial_max_stream_data_bidi_remote.value(trans_params(scid)).stream_pos_32);
        };
        if initial_max_data.is_set(trans_params(scid)) {
            call tls_api.upper.save_initial_max_data(initial_max_data.value(trans_params(scid)).stream_pos_32);
        };
        if initial_max_stream_data_bidi_local.is_set(trans_params(scid)) {
            call tls_api.upper.save_initial_max_stream_data_bidi_local(initial_max_stream_data_bidi_local.value(trans_params(scid)).stream_pos_32);
        };
        if initial_max_stream_id_bidi.is_set(trans_params(scid)) {
            call tls_api.upper.save_initial_max_stream_id_bidi(initial_max_stream_id_bidi.value(trans_params(scid)).stream_id_16);
        };
        if active_connection_id_limit.is_set(trans_params(scid)) {
            call tls_api.upper.save_active_connection_id_limit(active_connection_id_limit.value(trans_params(scid)).stream_pos_32);
        };
    }
}

import action show_enc_level(e:quic_packet_type)
import action max_idle_timeout_update(e:microseconds)
import action show_current_idle_timeout(e:microseconds)
import action show_probe_idle_timeout(e:microseconds)
import action show_probing_time(e:microseconds)
import action show_max_ack_delay(e:microseconds)
import action show_ack_delay_exponent(e:microseconds)
import action sleep_event(e:microseconds)
import action show_cond(e:bool)

import action show_cid(e:cid)

import action show_pstats(scid:cid,e:quic_packet_type,pnum:pkt_num)

import action show_ack_credit(c:cid,p: pkt_num,eli: bool,non_ack: bool, pp: pkt_num)

import action show_probing(c:cid,pp: pkt_num)