Ping packet

Here, we define functions for QUIC packet packet protection.

include ping_byte_stream
include collections
include ping_frame

module ping_array = {
    instance idx : unbounded_sequence
    instance arr : array(idx,stream_data)
}

object ping_packet = {
    type this = struct {
        payload : frame.arr
     }
    instance idx : unbounded_sequence
    instance arr : array(idx,this)
}

function ping_length  : stream_pos

function current_time : milliseconds
relation enough_wait

action ping_packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:ping_packet) = {}

import action show_current_time(now:milliseconds)

around ping_packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:ping_packet) {
    require num_queued_frames = 2; # [7]
    require pkt.payload = queued_frames;

    ...

    queued_frames := frame.arr.empty;
    num_queued_frames := 0;

timestamp_frame_pending := true;

}