8.  Header Formats (Normative)

   This section describes the set of compressed TCP/IP packet formats.
   The normative description of the packet formats is given using the
   formal notation for ROHC profiles defined in [RFC4997].  The formal
   description of the packet formats specifies all of the information
   needed to compress and decompress a header relative to the context.

   In particular, the notation provides a list of all the fields present
   in the uncompressed and compressed TCP/IP headers, and defines how to
   map from each uncompressed packet to its compressed equivalent and
   vice versa.

8.1.  Design Rationale for Compressed Base Headers

   The compressed header formats are defined as two separate sets: one
   set for the packets where the innermost IP header contains a
   sequential IP-ID (either network byte order or byte swapped), and one
   set for the packets without sequential IP-ID (either random, zero, or
   no IP-ID).

   These two sets of header formats are referred to as the "sequential"
   and the "random" set of header formats, respectively.

   In addition, there is one compressed format that is common to both
   sets of header formats and that can thus be used regardless of the
   type of IP-ID behavior.  This format can transmit rarely changing
   fields and also send the frequently changing fields coded in variable
   lengths.  It can also change the value of control fields such as
   IP-ID behavior and ECN behavior.

   All compressed base headers contain a 3-bit CRC, unless they update
   control fields such as "ip_id_behavior" or "ecn_used" that affect the
   interpretation of subsequent headers.  Headers that can modify these
   control fields carry a 7-bit CRC instead.

   When discussing LSB-encoded fields below, "p" equals the
   "offset_param" and "k" equals the "num_lsbs_param" in [RFC4997].  The
   encoding methods used in the compressed base headers are based on the
   following design criteria:

   o  MSN

         Since the MSN is a number generated by the compressor, it only
         needs to be large enough to ensure robust operation and to
         accommodate a small amount of reordering [RFC4163].  Therefore,
         each compressed base header has an MSN field that is LSB-
         encoded with k=4 and p=4 to handle a reordering depth of up to

         4 packets.  Additional guidance to improve robustness when
         reordering is possible can be found in [RFC4224].

   o  TCP Sequence Number

         ROHC-TCP has the capability to handle bulk data transfers
         efficiently, for which the sequence number is expected to
         increase by about 1460 octets (which can be represented by 11
         bits).  For the compressed base headers to handle
         retransmissions (i.e., negative delta to the sequence number),
         the LSB interpretation interval has to handle negative offsets
         about as large as positive offsets, which means that one more
         bit is needed.

         Also, for ROHC-TCP to be robust to losses, two additional bits
         are added to the LSB encoding of the sequence number.  This
         means that the base headers should contain at least 14 bits of
         LSB-encoded sequence number when present.  According to the
         logic above, the LSB offset value is set to be as large as the
         positive offset, i.e., p = 2^(k-1)-1.

   o  TCP Acknowledgment Number

         The design criterion for the acknowledgment number is similar
         to that of the TCP Sequence Number.  However, often only every
         other data packet is acknowledged, which means that the
         expected delta value is twice as large as for sequence numbers.

         Therefore, at least 15 bits of acknowledgment number should be
         used in compressed base headers.  Since the acknowledgment
         number is expected to constantly increase, and the only
         exception to this is packet reordering (either on the ROHC
         channel [RFC3759] or prior to the compression point), the
         negative offset for LSB encoding is set to be 1/4 of the total
         interval, i.e., p = 2^(k-2)-1.

   o  TCP Window

         The TCP Window field is expected to increase in increments of
         similar size as the TCP Sequence Number, and therefore the
         design criterion for the TCP window is to send at least 14 bits
         when used.

   o  IP-ID

         For the "sequential" set of packet formats, all the compressed
         base headers contain LSB-encoded IP-ID offset bits, where the
         offset is the difference between the value of the MSN field and

         the value of the IP-ID field.  The requirement is that at least
         3 bits of IP-ID should always be present, but it is preferable
         to use 4 to 7 bits.  When k=3 then p=1, and if k>3 then p=3
         since the offset is expected to increase most of the time.

   Each set of header formats contains eight different compressed base
   headers.  The reason for having this large number of header formats
   is that the TCP Sequence Number, TCP Acknowledgment Number, and TCP
   Window are frequently changing in a non-linear pattern.

   The design of the header formats is derived from the field behavior
   analysis found in [RFC4413].

   All of the compressed base headers transmit LSB-encoded MSN bits, the
   TCP Push flag, and a CRC, and in addition to this, all the base
   headers in the sequential packet format set contain LSB-encoded IP-ID
   bits.

   The following header formats exist in both the sequential and random
   packet format sets:

   o  Format 1: This header format carries changes to the TCP Sequence
      Number and is expected to be used on the downstream of a data
      transfer.

   o  Format 2: This header format carries the TCP Sequence Number in
      scaled form and is expected to be useful for the downstream of a
      data transfer where the payload size is constant for multiple
      packets.

   o  Format 3: This header format carries changes in the TCP
      Acknowledgment Number and is expected to be useful for the
      acknowledgment direction of a data transfer.

   o  Format 4: This header format is similar to format 3, but carries a
      scaled TCP Acknowledgment Number.

   o  Format 5: This header format carries both the TCP Sequence Number
      and the TCP Acknowledgment Number and is expected to be useful for
      flows that send data in both directions.

   o  Format 6: This header format is similar to format 5, but carries
      the TCP Sequence Number in scaled form, when the payload size is
      static for certain intervals in a data flow.

   o  Format 7: This header format carries changes to both the TCP
      Acknowledgment Number and the TCP Window and is expected to be
      useful for the acknowledgment flows of data connections.

   o  Format 8: This header format is used to convey changes to some of
      the more seldom changing fields in the TCP flow, such as ECN
      behavior, RST/SYN/FIN flags, the TTL/Hop Limit, and the TCP
      options list.  This format carries a 7-bit CRC, since it can
      change the structure of the contents of the irregular chain for
      subsequent packets.  Note that this can be seen as a reduced form
      of the common packet format.

   o  Common header format: The common header format can be used for all
      kinds of IP-ID behavior and should be useful when some of the more
      rarely changing fields in the IP or TCP header change.  Since this
      header format can update control fields that decide how the
      decompressor interprets packets, it carries a 7-bit CRC to reduce
      the probability of context corruption.  This header can basically
      convey changes to any of the dynamic fields in the IP and TCP
      headers, and it uses a large set of flags to provide information
      about which fields are present in the header format.

8.2.  Formal Definition of Header Formats

 ////////////////////////////////////////////
 // Constants
 ////////////////////////////////////////////

 IP_ID_BEHAVIOR_SEQUENTIAL = 0;
 IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED = 1;
 IP_ID_BEHAVIOR_RANDOM = 2;
 IP_ID_BEHAVIOR_ZERO = 3;

 ////////////////////////////////////////////
 // Global control fields
 ////////////////////////////////////////////

 CONTROL {
   ecn_used            [ 1 ];
   msn                 [ 16 ];
 }

 ///////////////////////////////////////////////
 // Encoding methods not specified in FN syntax
 ///////////////////////////////////////////////

 list_tcp_options               "defined in Section 6.3.3";
 inferred_ip_v4_header_checksum "defined in Section 6.4.1";
 inferred_mine_header_checksum  "defined in Section 6.4.2";
 inferred_ip_v4_length          "defined in Section 6.4.3";
 inferred_ip_v6_length          "defined in Section 6.4.4";
 inferred_offset                "defined in Section 6.4.5";

 baseheader_extension_headers   "defined in Section 6.4.6";
 baseheader_outer_headers       "defined in Section 6.4.7";

 ////////////////////////////////////////////
 // General encoding methods
 ////////////////////////////////////////////

 static_or_irreg(flag, width)
 {
   UNCOMPRESSED {
     field [ width ];
   }

   COMPRESSED irreg_enc {
     field =:= irregular(width) [ width ];
     ENFORCE(flag == 1);
   }

   COMPRESSED static_enc {
     field =:= static [ 0 ];
     ENFORCE(flag == 0);
   }
 }

 zero_or_irreg(flag, width)
 {
   UNCOMPRESSED {
     field [ width ];
   }

   COMPRESSED non_zero {
     field =:= irregular(width) [ width ];
     ENFORCE(flag == 0);
   }

   COMPRESSED zero {
     field =:= uncompressed_value(width, 0) [ 0 ];
     ENFORCE(flag == 1);
   }
 }

 variable_length_32_enc(flag)
 {
   UNCOMPRESSED {
     field [ 32 ];
   }

   COMPRESSED not_present {

     field =:= static [ 0 ];
     ENFORCE(flag == 0);
   }

   COMPRESSED lsb_8_bit {
     field =:= lsb(8, 63) [ 8 ];
     ENFORCE(flag == 1);
   }

   COMPRESSED lsb_16_bit {
     field =:= lsb(16, 16383) [ 16 ];
     ENFORCE(flag == 2);
   }

   COMPRESSED irreg_32_bit {
     field =:= irregular(32) [ 32 ];
     ENFORCE(flag == 3);
   }
 }

 optional32(flag)
 {
   UNCOMPRESSED {
     item [ 0, 32 ];
   }

   COMPRESSED present {
     item =:= irregular(32) [ 32 ];
     ENFORCE(flag == 1);
   }

   COMPRESSED not_present {
     item =:= compressed_value(0, 0) [ 0 ];
     ENFORCE(flag == 0);
   }
 }
 lsb_7_or_31
 {
   UNCOMPRESSED {
     item [ 32 ];
   }

   COMPRESSED lsb_7 {
     discriminator =:= '0'       [ 1 ];
     item          =:= lsb(7, 8) [ 7 ];
   }

   COMPRESSED lsb_31 {

     discriminator =:= '1'          [ 1 ];
     item          =:= lsb(31, 256) [ 31 ];
   }
 }

 opt_lsb_7_or_31(flag)
 {
   UNCOMPRESSED {
     item [ 0, 32 ];
   }

   COMPRESSED present {
     item =:= lsb_7_or_31 [ 8, 32 ];
     ENFORCE(flag == 1);
   }

   COMPRESSED not_present {
     item =:= compressed_value(0, 0) [ 0 ];
     ENFORCE(flag == 0);
   }
 }

 crc3(data_value, data_length)
 {
   UNCOMPRESSED {
   }

   COMPRESSED {
     crc_value =:=
       crc(3, 0x06, 0x07, data_value, data_length) [ 3 ];
   }
 }

 crc7(data_value, data_length)
 {
   UNCOMPRESSED {
   }

   COMPRESSED {
     crc_value =:=
       crc(7, 0x79, 0x7f, data_value, data_length) [ 7 ];
   }
 }

 one_bit_choice
 {
   UNCOMPRESSED {
     field [ 1 ];

   }

   COMPRESSED zero {
     field [ 1 ];
     ENFORCE(field.UVALUE == 0);
   }

   COMPRESSED nonzero {
     field [ 1 ];
     ENFORCE(field.UVALUE == 1);
   }
 }


 // Encoding method for updating a scaled field and its associated
 // control fields.  Should be used both when the value is scaled
 // or unscaled in a compressed format.
 field_scaling(stride_value, scaled_value, unscaled_value)
 {
   UNCOMPRESSED {
     residue_field [ 32 ];
   }

   COMPRESSED no_scaling {
     ENFORCE(stride_value == 0);
     ENFORCE(residue_field.UVALUE == unscaled_value);
     ENFORCE(scaled_value == 0);
   }

   COMPRESSED scaling_used {
     ENFORCE(stride_value != 0);
     ENFORCE(residue_field.UVALUE == (unscaled_value % stride_value));
     ENFORCE(unscaled_value ==
             scaled_value * stride_value + residue_field.UVALUE);
   }
 }
 ////////////////////////////////////////////
 // IPv6 Destination options header
 ////////////////////////////////////////////

 ip_dest_opt
 {
   UNCOMPRESSED {
     next_header [ 8 ];
     length      [ 8 ];
     value       [ length.UVALUE * 64 + 48 ];
   }

   DEFAULT {
     length      =:= static;
     next_header =:= static;
     value       =:= static;
   }

   COMPRESSED dest_opt_static {
     next_header =:= irregular(8) [ 8 ];
     length      =:= irregular(8) [ 8 ];
   }

   COMPRESSED dest_opt_dynamic {
     value =:=
       irregular(length.UVALUE * 64 + 48) [ length.UVALUE * 64 + 48 ];
   }

   COMPRESSED dest_opt_0_replicate {
     discriminator =:= '00000000' [ 8 ];
   }

   COMPRESSED dest_opt_1_replicate {
     discriminator =:= '10000000'                     [ 8 ];
     length        =:= irregular(8)                   [ 8 ];
     value         =:=
       irregular(length.UVALUE*64+48) [ length.UVALUE * 64 + 48 ];
   }

   COMPRESSED dest_opt_irregular {
   }
 }

 ////////////////////////////////////////////
 // IPv6 Hop-by-Hop options header
 ////////////////////////////////////////////

 ip_hop_opt
 {
   UNCOMPRESSED {
     next_header [ 8 ];
     length      [ 8 ];
     value       [ length.UVALUE * 64 + 48 ];
   }

   DEFAULT {
     length      =:= static;
     next_header =:= static;
     value       =:= static;
   }

   COMPRESSED hop_opt_static {
     next_header =:= irregular(8) [ 8 ];
     length      =:= irregular(8) [ 8 ];
   }

   COMPRESSED hop_opt_dynamic {
     value =:=
       irregular(length.UVALUE*64+48) [ length.UVALUE * 64 + 48 ];
   }

   COMPRESSED hop_opt_0_replicate {
     discriminator =:= '00000000' [ 8 ];
   }

   COMPRESSED hop_opt_1_replicate {
     discriminator =:= '10000000'                     [ 8 ];
     length        =:= irregular(8)                   [ 8 ];
     value         =:=
       irregular(length.UVALUE*64+48) [ length.UVALUE * 64 + 48 ];
   }

   COMPRESSED hop_opt_irregular {
   }
 }

 ////////////////////////////////////////////
 // IPv6 Routing header
 ////////////////////////////////////////////

 ip_rout_opt
 {
   UNCOMPRESSED {
     next_header [ 8 ];
     length      [ 8 ];
     value       [ length.UVALUE * 64 + 48 ];
   }

   DEFAULT {
     length      =:= static;
     next_header =:= static;
     value       =:= static;
   }

   COMPRESSED rout_opt_static {
     next_header =:= irregular(8)                   [ 8 ];
     length      =:= irregular(8)                   [ 8 ];
     value       =:=
       irregular(length.UVALUE*64+48) [ length.UVALUE * 64 + 48 ];

   }

   COMPRESSED rout_opt_dynamic {
   }

   COMPRESSED rout_opt_0_replicate {
     discriminator =:= '00000000' [ 8 ];
   }

   COMPRESSED rout_opt_0_replicate {
     discriminator =:= '10000000'                     [ 8 ];
     length        =:= irregular(8)                   [ 8 ];
     value         =:=
       irregular(length.UVALUE*64+48) [ length.UVALUE * 64 + 48 ];
   }

   COMPRESSED rout_opt_irregular {
   }
 }

 ////////////////////////////////////////////
 // GRE Header
 ////////////////////////////////////////////

 optional_checksum(flag_value)
 {
   UNCOMPRESSED {
     value     [ 0, 16 ];
     reserved1 [ 0, 16 ];
   }

   COMPRESSED cs_present {
     value     =:= irregular(16)             [ 16 ];
     reserved1 =:= uncompressed_value(16, 0) [ 0 ];
     ENFORCE(flag_value == 1);
   }

   COMPRESSED not_present {
     value     =:= compressed_value(0, 0) [ 0 ];
     reserved1 =:= compressed_value(0, 0) [ 0 ];
     ENFORCE(flag_value == 0);
   }
 }

 gre_proto
 {
   UNCOMPRESSED {
     protocol [ 16 ];

   }

   COMPRESSED ether_v4 {
     discriminator =:= compressed_value(1, 0)         [ 1 ];
     protocol      =:= uncompressed_value(16, 0x0800) [ 0 ];
   }

   COMPRESSED ether_v6 {
     discriminator =:= compressed_value(1, 1)         [ 1 ];
     protocol      =:= uncompressed_value(16, 0x86DD) [ 0 ];
   }
 }

 gre
 {
   UNCOMPRESSED {
     c_flag                                 [ 1 ];
     r_flag    =:= uncompressed_value(1, 0) [ 1 ];
     k_flag                                 [ 1 ];
     s_flag                                 [ 1 ];
     reserved0 =:= uncompressed_value(9, 0) [ 9 ];
     version   =:= uncompressed_value(3, 0) [ 3 ];
     protocol                               [ 16 ];
     checksum_and_res                       [ 0, 32 ];
     key                                    [ 0, 32 ];
     sequence_number                        [ 0, 32 ];
   }

   DEFAULT {
     c_flag           =:= static;
     k_flag           =:= static;
     s_flag           =:= static;
     protocol         =:= static;
     key              =:= static;
     sequence_number  =:= static;
   }

   COMPRESSED gre_static {
     protocol =:= gre_proto                 [ 1 ];
     c_flag   =:= irregular(1)              [ 1 ];
     k_flag   =:= irregular(1)              [ 1 ];
     s_flag   =:= irregular(1)              [ 1 ];
     padding  =:= compressed_value(4, 0)    [ 4 ];
     key      =:= optional32(k_flag.UVALUE) [ 0, 32 ];
   }

   COMPRESSED gre_dynamic {
     checksum_and_res =:=

       optional_checksum(c_flag.UVALUE)             [ 0, 16 ];
     sequence_number  =:= optional32(s_flag.UVALUE) [ 0, 32 ];
   }

   COMPRESSED gre_0_replicate {
     discriminator    =:= '00000000'    [ 8 ];
     checksum_and_res =:=
       optional_checksum(c_flag.UVALUE) [ 0, 16 ];
     sequence_number  =:=
       optional32(s_flag.UVALUE)        [ 0, 8, 32 ];
   }

   COMPRESSED gre_1_replicate {
     discriminator    =:= '10000'                   [ 5 ];
     c_flag           =:= irregular(1)              [ 1 ];
     k_flag           =:= irregular(1)              [ 1 ];
     s_flag           =:= irregular(1)              [ 1 ];
     checksum_and_res =:=
       optional_checksum(c_flag.UVALUE)             [ 0, 16 ];
     key              =:= optional32(k_flag.UVALUE) [ 0, 32 ];
     sequence_number  =:= optional32(s_flag.UVALUE) [ 0, 32 ];
   }

   COMPRESSED gre_irregular {
     checksum_and_res =:=
       optional_checksum(c_flag.UVALUE) [ 0, 16 ];
     sequence_number  =:=
       opt_lsb_7_or_31(s_flag.UVALUE)   [ 0, 8, 32 ];
   }
 }

 /////////////////////////////////////////////
 // MINE header
 /////////////////////////////////////////////

 mine
 {
   UNCOMPRESSED {
     next_header [ 8 ];
     s_bit       [ 1 ];
     res_bits    [ 7 ];
     checksum    [ 16 ];
     orig_dest   [ 32 ];
     orig_src    [ 0, 32 ];
   }

   DEFAULT {
     next_header =:= static;

     s_bit       =:= static;
     res_bits    =:= static;
     checksum    =:= inferred_mine_header_checksum;
     orig_dest   =:= static;
     orig_src    =:= static;
   }

   COMPRESSED mine_static {
     next_header =:= irregular(8)             [ 8 ];
     s_bit       =:= irregular(1)             [ 1 ];
     // Reserved bits are included to achieve byte-alignment
     res_bits    =:= irregular(7)             [ 7 ];
     orig_dest   =:= irregular(32)            [ 32 ];
     orig_src    =:= optional32(s_bit.UVALUE) [ 0, 32 ];
   }

   COMPRESSED mine_dynamic {
   }

   COMPRESSED mine_0_replicate {
     discriminator =:= '00000000' [ 8 ];
   }

   COMPRESSED mine_1_replicate {
     discriminator =:= '10000000'               [ 8 ];
     s_bit         =:= irregular(1)             [ 1 ];
     res_bits      =:= irregular(7)             [ 7 ];
     orig_dest     =:= irregular(32)            [ 32 ];
     orig_src      =:= optional32(s_bit.UVALUE) [ 0, 32 ];
   }

   COMPRESSED mine_irregular {
   }
 }

 /////////////////////////////////////////////
 // Authentication Header (AH)
 /////////////////////////////////////////////

 ah
 {
   UNCOMPRESSED {
     next_header     [ 8 ];
     length          [ 8 ];
     res_bits        [ 16 ];
     spi             [ 32 ];
     sequence_number [ 32 ];
     auth_data       [ length.UVALUE*32-32 ];

   }

   DEFAULT {
     next_header     =:= static;
     length          =:= static;
     res_bits        =:= static;
     spi             =:= static;
     sequence_number =:= static;
   }

   COMPRESSED ah_static {
     next_header =:= irregular(8)  [ 8 ];
     length      =:= irregular(8)  [ 8 ];
     spi         =:= irregular(32) [ 32 ];
   }

   COMPRESSED ah_dynamic {
     res_bits        =:= irregular(16) [ 16 ];
     sequence_number =:= irregular(32) [ 32 ];
     auth_data       =:=
       irregular(length.UVALUE*32-32)  [ length.UVALUE*32-32 ];
   }

   COMPRESSED ah_0_replicate {
     discriminator   =:= '00000000'    [ 8 ];
     sequence_number =:= irregular(32) [ 32 ];
     auth_data       =:=
       irregular(length.UVALUE*32-32)  [ length.UVALUE*32-32 ];
   }

   COMPRESSED ah_1_replicate {
     discriminator   =:= '10000000'    [ 8 ];
     length          =:= irregular(8)  [ 8 ];
     res_bits        =:= irregular(16) [ 16 ];
     spi             =:= irregular(32) [ 32 ];
     sequence_number =:= irregular(32) [ 32 ];
     auth_data       =:=
       irregular(length.UVALUE*32-32)  [ length.UVALUE*32-32 ];
   }

   COMPRESSED ah_irregular {
     sequence_number =:= lsb_7_or_31  [ 8, 32 ];
     auth_data       =:=
       irregular(length.UVALUE*32-32) [ length.UVALUE*32-32 ];
   }
 }

 /////////////////////////////////////////////

 // ESP header (NULL encrypted)
 /////////////////////////////////////////////

 // The value of the Next Header field from the trailer
 // part of the packet is passed as a parameter.
 esp_null(next_header_value)
 {
   UNCOMPRESSED {
     spi             [ 32 ];
     sequence_number [ 32 ];
   }

   CONTROL {
     nh_field [ 8 ];
   }

   DEFAULT {
     spi             =:= static;
     sequence_number =:= static;
     nh_field        =:= static;
   }

   COMPRESSED esp_static {
     nh_field =:= compressed_value(8, next_header_value) [ 8 ];
     spi      =:= irregular(32)                          [ 32 ];
   }

   COMPRESSED esp_dynamic {
     sequence_number =:= irregular(32) [ 32 ];
   }

   COMPRESSED esp_0_replicate {
     discriminator   =:= '00000000'    [ 8 ];
     sequence_number =:= irregular(32) [ 32 ];
   }
   COMPRESSED esp_1_replicate {
     discriminator   =:= '10000000'    [ 8 ];
     spi             =:= irregular(32) [ 32 ];
     sequence_number =:= irregular(32) [ 32 ];
   }

   COMPRESSED esp_irregular {
     sequence_number =:= lsb_7_or_31 [ 8, 32 ];
   }
 }

 /////////////////////////////////////////////
 // IPv6 Header

 /////////////////////////////////////////////

 fl_enc
 {
   UNCOMPRESSED {
     flow_label [ 20 ];
   }

   COMPRESSED fl_zero {
     discriminator =:= '0'                       [ 1 ];
     flow_label    =:= uncompressed_value(20, 0) [ 0 ];
     reserved      =:= '0000'                    [ 4 ];
   }

   COMPRESSED fl_non_zero {
     discriminator =:= '1'           [ 1 ];
     flow_label    =:= irregular(20) [ 20 ];
   }
 }

 // The is_innermost flag is true if this is the innermost IP header
 // If extracting the irregular chain for a compressed packet:
 //   - ttl_irregular_chain_flag must have the same value as it had when
 //     processing co_baseheader.
 //   - ip_inner_ecn is bound in this encoding method and the value that
 //     it gets bound to should be passed to the tcp encoding method
 //   For other formats than the irregular chain, these two are ignored
 ipv6(is_innermost, ttl_irregular_chain_flag, ip_inner_ecn)
 {
   UNCOMPRESSED {
     version         =:= uncompressed_value(4, 6) [ 4 ];
     dscp                                         [ 6 ];
     ip_ecn_flags                                 [ 2 ];
     flow_label                                   [ 20 ];
     payload_length                               [ 16 ];
     next_header                                  [ 8 ];
     ttl_hopl                                     [ 8 ];
     src_addr                                     [ 128 ];
     dst_addr                                     [ 128 ];
   }

   DEFAULT {
     dscp           =:= static;
     ip_ecn_flags   =:= static;
     flow_label     =:= static;
     payload_length =:= inferred_ip_v6_length;
     next_header    =:= static;
     ttl_hopl       =:= static;

     src_addr       =:= static;
     dst_addr       =:= static;
   }

   COMPRESSED ipv6_static {
     version_flag =:= '1'            [ 1 ];
     reserved     =:= '00'           [ 2 ];
     flow_label   =:= fl_enc         [ 5, 21 ];
     next_header  =:= irregular(8)   [ 8 ];
     src_addr     =:= irregular(128) [ 128 ];
     dst_addr     =:= irregular(128) [ 128 ];
   }

   COMPRESSED ipv6_dynamic {
     dscp         =:= irregular(6) [ 6 ];
     ip_ecn_flags =:= irregular(2) [ 2 ];
     ttl_hopl     =:= irregular(8) [ 8 ];
   }

   COMPRESSED ipv6_replicate {
     dscp         =:= irregular(6) [ 6 ];
     ip_ecn_flags =:= irregular(2) [ 2 ];
     reserved     =:= '000'        [ 3 ];
     flow_label   =:= fl_enc       [ 5, 21 ];
   }

   COMPRESSED ipv6_outer_without_ttl_irregular {
     dscp         =:= static_or_irreg(ecn_used.UVALUE, 6) [ 0, 6 ];
     ip_ecn_flags =:= static_or_irreg(ecn_used.UVALUE, 2) [ 0, 2 ];
     ENFORCE(ttl_irregular_chain_flag == 0);
     ENFORCE(is_innermost == false);
   }

   COMPRESSED ipv6_outer_with_ttl_irregular {
     dscp         =:= static_or_irreg(ecn_used.UVALUE, 6) [ 0, 6 ];
     ip_ecn_flags =:= static_or_irreg(ecn_used.UVALUE, 2) [ 0, 2 ];
     ttl_hopl     =:= irregular(8)                        [ 8 ];
     ENFORCE(ttl_irregular_chain_flag == 1);
     ENFORCE(is_innermost == false);
   }

   COMPRESSED ipv6_innermost_irregular {
     ENFORCE(ip_inner_ecn == ip_ecn_flags.UVALUE);
     ENFORCE(is_innermost == true);
   }
 }

 /////////////////////////////////////////////

 // IPv4 Header
 /////////////////////////////////////////////

 ip_id_enc_dyn(behavior)
 {
   UNCOMPRESSED {
     ip_id [ 16 ];
   }

   COMPRESSED ip_id_seq {
     ip_id =:= irregular(16) [ 16 ];
     ENFORCE((behavior == IP_ID_BEHAVIOR_SEQUENTIAL) ||
             (behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED) ||
             (behavior == IP_ID_BEHAVIOR_RANDOM));
   }

   COMPRESSED ip_id_zero {
     ip_id =:= uncompressed_value(16, 0) [ 0 ];
     ENFORCE(behavior == IP_ID_BEHAVIOR_ZERO);
   }
 }

 ip_id_enc_irreg(behavior)
 {
   UNCOMPRESSED {
     ip_id [ 16 ];
   }

   COMPRESSED ip_id_seq {
     ENFORCE(behavior == IP_ID_BEHAVIOR_SEQUENTIAL);
   }

   COMPRESSED ip_id_seq_swapped {
     ENFORCE(behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED);
   }
   COMPRESSED ip_id_rand {
     ip_id =:= irregular(16) [ 16 ];
     ENFORCE(behavior == IP_ID_BEHAVIOR_RANDOM);
   }

   COMPRESSED ip_id_zero {
     ip_id =:= uncompressed_value(16, 0) [ 0 ];
     ENFORCE(behavior == IP_ID_BEHAVIOR_ZERO);
   }
 }

 ip_id_behavior_choice(is_inner)
 {

   UNCOMPRESSED {
     behavior [ 2 ];
   }

   DEFAULT {
     behavior =:= irregular(2);
   }

   COMPRESSED sequential {
     behavior [ 2 ];
     ENFORCE(is_inner == true);
     ENFORCE(behavior.UVALUE == IP_ID_BEHAVIOR_SEQUENTIAL);
   }

   COMPRESSED sequential_swapped {
     behavior [ 2 ];
     ENFORCE(is_inner == true);
     ENFORCE(behavior.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED);
   }

   COMPRESSED random {
     behavior [ 2 ];
     ENFORCE(behavior.UVALUE == IP_ID_BEHAVIOR_RANDOM);
   }

   COMPRESSED zero {
     behavior [ 2 ];
     ENFORCE(behavior.UVALUE == IP_ID_BEHAVIOR_ZERO);
   }
 }

 // The is_innermost flag is true if this is the innermost IP header
 // If extracting the irregular chain for a compressed packet:
 //   - ttl_irregular_chain_flag must have the same value as it had when
 //     processing co_baseheader.
 //   - ip_inner_ecn is bound in this encoding method and the value that
 //     it gets bound to should be passed to the tcp encoding method
 //   For other formats than the irregular chain, these two are ignored
 ipv4(is_innermost, ttl_irregular_chain_flag, ip_inner_ecn)
 {
   UNCOMPRESSED {
     version        =:= uncompressed_value(4, 4)  [ 4 ];
     hdr_length     =:= uncompressed_value(4, 5)  [ 4 ];
     dscp                                         [ 6 ];
     ip_ecn_flags                                 [ 2 ];
     length                                       [ 16 ];
     ip_id                                        [ 16 ];

     rf             =:= uncompressed_value(1, 0)  [ 1 ];
     df                                           [ 1 ];
     mf             =:= uncompressed_value(1, 0)  [ 1 ];
     frag_offset    =:= uncompressed_value(13, 0) [ 13 ];
     ttl_hopl                                     [ 8 ];
     protocol                                     [ 8 ];
     checksum                                     [ 16 ];
     src_addr                                     [ 32 ];
     dst_addr                                     [ 32 ];
   }

   CONTROL {
     ip_id_behavior [ 2 ];
   }

   DEFAULT {
     dscp           =:= static;
     ip_ecn_flags   =:= static;
     length         =:= inferred_ip_v4_length;
     df             =:= static;
     ttl_hopl       =:= static;
     protocol       =:= static;
     checksum       =:= inferred_ip_v4_header_checksum;
     src_addr       =:= static;
     dst_addr       =:= static;
     ip_id_behavior =:= static;
   }

   COMPRESSED ipv4_static {
     version_flag =:= '0'           [ 1 ];
     reserved     =:= '0000000'     [ 7 ];
     protocol     =:= irregular(8)  [ 8 ];
     src_addr     =:= irregular(32) [ 32 ];
     dst_addr     =:= irregular(32) [ 32 ];
   }

   COMPRESSED ipv4_dynamic {
     reserved       =:= '00000'             [ 5 ];
     df             =:= irregular(1)        [ 1 ];
     ip_id_behavior =:= ip_id_behavior_choice(is_innermost) [ 2 ];
     dscp           =:= irregular(6)        [ 6 ];
     ip_ecn_flags   =:= irregular(2)        [ 2 ];
     ttl_hopl       =:= irregular(8)        [ 8 ];
     ip_id          =:=
       ip_id_enc_dyn(ip_id_behavior.UVALUE) [ 0, 16 ];
   }

   COMPRESSED ipv4_replicate {

     reserved       =:= '0000'              [ 4 ];
     ip_id_behavior =:= ip_id_behavior_choice(is_innermost) [ 2 ];
     ttl_flag       =:= irregular(1)        [ 1 ];
     df             =:= irregular(1)        [ 1 ];
     dscp           =:= irregular(6)        [ 6 ];
     ip_ecn_flags   =:= irregular(2)        [ 2 ];
     ip_id          =:=
       ip_id_enc_dyn(ip_id_behavior.UVALUE) [ 0, 16 ];
     ttl_hopl     =:=
         static_or_irreg(ttl_flag.UVALUE, 8) [ 0, 8 ];
   }

   COMPRESSED ipv4_outer_without_ttl_irregular {
     ip_id        =:=
       ip_id_enc_irreg(ip_id_behavior.UVALUE) [ 0, 16 ];
     dscp         =:= static_or_irreg(ecn_used.UVALUE, 6) [ 0, 6 ];
     ip_ecn_flags =:= static_or_irreg(ecn_used.UVALUE, 2) [ 0, 2 ];
     ENFORCE(ttl_irregular_chain_flag == 0);
     ENFORCE(is_innermost == false);
   }

   COMPRESSED ipv4_outer_with_ttl_irregular {
     ip_id        =:=
       ip_id_enc_irreg(ip_id_behavior.UVALUE)             [ 0, 16 ];
     dscp         =:= static_or_irreg(ecn_used.UVALUE, 6) [ 0, 6 ];
     ip_ecn_flags =:= static_or_irreg(ecn_used.UVALUE, 2) [ 0, 2 ];
     ttl_hopl     =:= irregular(8)                        [ 8 ];
     ENFORCE(is_innermost == false);
     ENFORCE(ttl_irregular_chain_flag == 1);
   }

   COMPRESSED ipv4_innermost_irregular {
     ip_id          =:=
       ip_id_enc_irreg(ip_id_behavior.UVALUE) [ 0, 16 ];
     ENFORCE(ip_inner_ecn == ip_ecn_flags.UVALUE);
     ENFORCE(is_innermost == true);
   }
 }

 /////////////////////////////////////////////
 // TCP Options
 /////////////////////////////////////////////

 // nbits is bound to the remaining length (in bits) of TCP
 // options, including the EOL type byte.
 tcp_opt_eol(nbits)
 {
   UNCOMPRESSED {

     type     =:= uncompressed_value(8, 0) [ 8 ];
     padding  =:=
       uncompressed_value(nbits-8, 0)      [ nbits-8 ];
   }

   CONTROL {
     pad_len [ 8 ];
   }

   COMPRESSED eol_list_item {
     pad_len =:= compressed_value(8, nbits-8) [ 8 ];
   }

   COMPRESSED eol_irregular {
     pad_len =:= static;
     ENFORCE(nbits-8 == pad_len.UVALUE);
   }
 }

 tcp_opt_nop
 {
   UNCOMPRESSED {
     type =:= uncompressed_value(8, 1) [ 8 ];
   }

   COMPRESSED nop_list_item {
   }

   COMPRESSED nop_irregular {
   }
 }

 tcp_opt_mss
 {
   UNCOMPRESSED {
     type   =:= uncompressed_value(8, 2) [ 8 ];
     length =:= uncompressed_value(8, 4) [ 8 ];
     mss                                 [ 16 ];
   }

   COMPRESSED mss_list_item {
     mss =:= irregular(16) [ 16 ];
   }

   COMPRESSED mss_irregular {
     mss    =:= static;
   }
 }