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

ah
{
  UNCOMPRESSED {
    next_header     [ 8 ];
    length          [ 8 ];
    res_bits        [ 16 ];
    spi             [ 32 ];
    sequence_number [ 32 ];
    icv             [ 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 ];
    icv       =:=
      irregular(length.UVALUE*32-32)  [ length.UVALUE*32-32 ];
  }

  COMPRESSED ah_0_replicate {
    discriminator   =:= '00000000'    [ 8 ];
    sequence_number =:= irregular(32) [ 32 ];
    icv             =:=
      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 ];
    icv             =:=
      irregular(length.UVALUE*32-32)  [ length.UVALUE*32-32 ];
  }

  COMPRESSED ah_irregular {
    sequence_number =:= lsb_7_or_31  [ 8, 32 ];
    icv       =:=
      irregular(length.UVALUE*32-32) [ length.UVALUE*32-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 {
    ENFORCE((behavior == IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    ENFORCE(ip_id_offset.UVALUE == ip_id.UVALUE - msn.UVALUE);
    ip_id =:= irregular(16) [ 16 ];
  }

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

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

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);
  }
}

// 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,
     ip_id_behavior_value)
{
  UNCOMPRESSED {
    version        =:= uncompressed_value(4, 4)  [ 4 ];
    hdr_length     =:= uncompressed_value(4, 5)  [ 4 ];
    dscp                                         [ 6 ];
    ip_ecn_flags                                 [ 2 ];
    length         =:= inferred_ip_v4_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    =:= inferred_ip_v4_header_checksum [ 16 ];
    src_addr                                     [ 32 ];
    dst_addr                                     [ 32 ];
  }

  CONTROL {
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);

    ENFORCE(innermost_ip.UVALUE == is_innermost);
    ip_id_behavior_outer [ 2 ];
    innermost_ip [ 1 ];
  }

  DEFAULT {
    dscp           =:= static;
    ip_ecn_flags   =:= static;
    df             =:= static;
    ttl_hopl       =:= static;
    protocol       =:= static;
    src_addr       =:= static;
    dst_addr       =:= static;
    ip_id_behavior_outer =:= 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_innermost_dynamic {
    ENFORCE(is_innermost == 1);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    reserved       =:= '00000'             [ 5 ];
    df             =:= irregular(1)        [ 1 ];
    ip_id_behavior_innermost =:= irregular(2) [ 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_innermost.UVALUE) [ 0, 16 ];
  }

  COMPRESSED ipv4_outer_dynamic {
    ENFORCE(is_innermost == 0);
    ENFORCE(ip_id_behavior_outer.UVALUE == ip_id_behavior_value);
    reserved       =:= '00000'             [ 5 ];
    df             =:= irregular(1)        [ 1 ];
    ip_id_behavior_outer =:=     irregular(2)              [ 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_outer.UVALUE) [ 0, 16 ];

  }

  COMPRESSED ipv4_innermost_replicate {
    ENFORCE(is_innermost == 1);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    reserved       =:= '0000'              [ 4 ];
    ip_id_behavior_innermost =:= irregular(2) [ 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_innermost.UVALUE) [ 0, 16 ];
    ttl_hopl     =:=
        static_or_irreg(ttl_flag.UVALUE, 8) [ 0, 8 ];
  }

  COMPRESSED ipv4_outer_replicate {
    ENFORCE(is_innermost == 0);
    ENFORCE(ip_id_behavior_outer.UVALUE == ip_id_behavior_value);
    reserved       =:= '0000'              [ 4 ];
    ip_id_behavior_outer =:= irregular(2)  [ 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_outer.UVALUE) [ 0, 16 ];
    ttl_hopl     =:=
        static_or_irreg(ttl_flag.UVALUE, 8) [ 0, 8 ];
  }

  COMPRESSED ipv4_outer_without_ttl_irregular {
    ENFORCE(is_innermost == 0);
    ip_id        =:=
      ip_id_enc_irreg(ip_id_behavior_outer.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);
  }

  COMPRESSED ipv4_outer_with_ttl_irregular {
    ENFORCE(is_innermost == 0);
    ip_id        =:=
      ip_id_enc_irreg(ip_id_behavior_outer.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(ttl_irregular_chain_flag == 1);
  }

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

/////////////////////////////////////////////
// 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;
  }
}

tcp_opt_wscale
{
  UNCOMPRESSED {
    type   =:= uncompressed_value(8, 3) [ 8 ];
    length =:= uncompressed_value(8, 3) [ 8 ];
    wscale                              [ 8 ];
  }

  COMPRESSED wscale_list_item {
    wscale =:= irregular(8) [ 8 ];
  }

  COMPRESSED wscale_irregular {
    wscale =:= static;
  }
}

ts_lsb
{
  UNCOMPRESSED {
    tsval [ 32 ];
  }

  COMPRESSED tsval_7 {
    discriminator =:= '0'        [ 1 ];
    tsval         =:= lsb(7, -1) [ 7 ];
  }

  COMPRESSED tsval_14 {
    discriminator =:= '10'        [ 2 ];
    tsval         =:= lsb(14, -1) [ 14 ];
  }

  COMPRESSED tsval_21 {
    discriminator =:= '110'               [ 3 ];
    tsval         =:= lsb(21, 0x00040000) [ 21 ];
  }

  COMPRESSED tsval_29 {
    discriminator =:= '111'               [ 3 ];
    tsval         =:= lsb(29, 0x04000000) [ 29 ];
  }
}

tcp_opt_ts
{
  UNCOMPRESSED {
    type   =:= uncompressed_value(8, 8)  [ 8 ];
    length =:= uncompressed_value(8, 10) [ 8 ];
    tsval                                [ 32 ];
    tsecho                               [ 32 ];
  }
  COMPRESSED tsopt_list_item {
    tsval  =:= irregular(32) [ 32 ];
    tsecho =:= irregular(32) [ 32 ];
  }

  COMPRESSED tsopt_irregular {
    tsval  =:= ts_lsb [ 8, 16, 24, 32 ];
    tsecho =:= ts_lsb [ 8, 16, 24, 32 ];
  }
}
sack_pure_lsb(base)
{
  UNCOMPRESSED {
    sack_field [ 32 ];
  }

  CONTROL {
    ENFORCE(sack_field.CVALUE == (sack_field.UVALUE - base));
  }

  COMPRESSED lsb_15 {
    ENFORCE(sack_field.CVALUE == sack_field.CVALUE <= 0x7fff);
    discriminator =:= '0'           [ 1 ];
    sack_field                      [ 15 ];

  }

  COMPRESSED lsb_22 {
    ENFORCE(sack_field.CVALUE == sack_field.CVALUE <= 0x3fffff);
    discriminator =:= '10'          [ 2 ];
    sack_field                      [ 22 ];
  }

  COMPRESSED lsb_29 {
    ENFORCE(sack_field.CVALUE == sack_field.CVALUE <= 0x1fffffff);
    discriminator =:= '110'         [ 3 ];
    sack_field                      [ 29 ];
  }

  COMPRESSED full_offset {
    discriminator =:= '11111111'    [ 8 ];
    sack_field                      [ 32 ];
  }
}

sack_block(reference)
{
  UNCOMPRESSED {
    block_start [ 32 ];
    block_end   [ 32 ];
  }

  COMPRESSED {
    block_start =:=
      sack_pure_lsb(reference)          [ 16, 24, 32, 40 ];
    block_end   =:=
      sack_pure_lsb(block_start.UVALUE) [ 16, 24, 32, 40 ];
  }
}

// The value of the parameter is set to the ack_number value
// of the TCP header
tcp_opt_sack(ack_value)
{

  UNCOMPRESSED {
    type    =:= uncompressed_value(8, 5) [ 8 ];
    length                               [ 8 ];
    block_1                              [ 64 ];
    block_2                              [ 0, 64 ];
    block_3                              [ 0, 64 ];
    block_4                              [ 0, 64 ];
  }

  DEFAULT {
    length  =:= static;
    block_2 =:= uncompressed_value(0, 0);
    block_3 =:= uncompressed_value(0, 0);
    block_4 =:= uncompressed_value(0, 0);
  }

  COMPRESSED sack1_list_item {
    discriminator =:= '00000001';
    block_1       =:= sack_block(ack_value);
    ENFORCE(length.UVALUE == 10);
  }

  COMPRESSED sack2_list_item {
    discriminator =:= '00000010';
    block_1       =:= sack_block(ack_value);
    block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
    ENFORCE(length.UVALUE == 18);
  }

COMPRESSED sack3_list_item {
   discriminator =:= '00000011';
   block_1       =:= sack_block(ack_value);
   block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   block_3       =:= sack_block(block_2.UVALUE && 0xFFFFFFFF);
   ENFORCE(length.UVALUE == 26);
 }

 COMPRESSED sack4_list_item {
   discriminator =:= '00000100';
   block_1       =:= sack_block(ack_value);
   block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   block_3       =:= sack_block(block_2.UVALUE && 0xFFFFFFFF);
   block_4       =:= sack_block(block_3.UVALUE && 0xFFFFFFFF);
   ENFORCE(length.UVALUE == 34);
 }

  COMPRESSED sack_unchanged_irregular {
    discriminator =:= '00000000';
    block_1       =:= static;
    block_2       =:= static;
    block_3       =:= static;
    block_4       =:= static;
  }

  COMPRESSED sack1_irregular {
    discriminator =:= '00000001';
    block_1       =:= sack_block(ack_value);

    ENFORCE(length.UVALUE == 10);
  }

 COMPRESSED sack2_irregular {
   discriminator =:= '00000010';
   block_1       =:= sack_block(ack_value);
   block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   ENFORCE(length.UVALUE == 18);
 }

 COMPRESSED sack3_irregular {
   discriminator =:= '00000011';
   block_1       =:= sack_block(ack_value);
   block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   block_3       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   ENFORCE(length.UVALUE == 26);
 }

 COMPRESSED sack4_irregular {
   discriminator =:= '00000100';
   block_1       =:= sack_block(ack_value);
   block_2       =:= sack_block(block_1.UVALUE && 0xFFFFFFFF);
   block_3       =:= sack_block(block_2.UVALUE && 0xFFFFFFFF);
   block_4       =:= sack_block(block_3.UVALUE && 0xFFFFFFFF);
   ENFORCE(length.UVALUE == 34);
 }
}

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

  COMPRESSED sack_permitted_list_item {
  }

  COMPRESSED sack_permitted_irregular {
  }
}

tcp_opt_generic
{
  UNCOMPRESSED {
    type                                    [ 8 ];
    length_msb =:= uncompressed_value(1, 0) [ 1 ];
    length_lsb                              [ 7 ];

    contents                           [ length_lsb.UVALUE*8-16 ];
  }

  CONTROL {
    option_static [ 1 ];
  }

  DEFAULT {
    type       =:= static;
    length_lsb =:= static;
    contents   =:= static;
  }

  COMPRESSED generic_list_item {
    type          =:= irregular(8)      [ 8 ];
    option_static =:= one_bit_choice    [ 1 ];
    length_lsb    =:= irregular(7)      [ 7 ];
    contents      =:=
      irregular(length_lsb.UVALUE*8-16) [ length_lsb.UVALUE*8-16 ];
  }

  // Used when context of option has option_static set to one
  COMPRESSED generic_static_irregular {
    ENFORCE(option_static.UVALUE == 1);
  }

  // An item that can change, but currently is unchanged
  COMPRESSED generic_stable_irregular {
    discriminator =:= '11111111' [ 8 ];
    ENFORCE(option_static.UVALUE == 0);
  }

  // An item that is assumed to change constantly.
  // Length is not allowed to change here, since a length change is
  // most likely to cause new NOPs or an EOL length change.
  COMPRESSED generic_full_irregular {
    discriminator =:= '00000000'        [ 8 ];
    contents      =:=
      irregular(length_lsb.UVALUE*8-16) [ length_lsb.UVALUE*8-16 ];
    ENFORCE(option_static.UVALUE == 0);
  }
}

tcp_list_presence_enc(presence)
{
  UNCOMPRESSED {
    tcp_options;
  }

  COMPRESSED list_not_present {
    tcp_options =:= static [ 0 ];
    ENFORCE(presence == 0);
  }

  COMPRESSED list_present {
    tcp_options =:= list_tcp_options [ VARIABLE ];
    ENFORCE(presence == 1);
  }
}

/////////////////////////////////////////////
// TCP Header
/////////////////////////////////////////////

port_replicate(flags)
{
  UNCOMPRESSED {
    port [ 16 ];
  }

  COMPRESSED port_static_enc {
    port =:= static [ 0 ];
    ENFORCE(flags == 0b00);
  }

  COMPRESSED port_lsb8 {
    port =:= lsb(8, 64) [ 8 ];
    ENFORCE(flags == 0b01);
  }

  COMPRESSED port_irr_enc {
    port =:= irregular(16) [ 16 ];
    ENFORCE(flags == 0b10);
  }
}

tcp_irreg_ip_ecn(ip_inner_ecn)
{
  UNCOMPRESSED {
    ip_ecn_flags [ 2 ];
  }

  COMPRESSED ecn_present {
    // This field does not exist in the uncompressed header
    // and therefore cannot use uncompressed_value.
    ip_ecn_flags =:=
      compressed_value(2, ip_inner_ecn) [ 2 ];

    ENFORCE(ecn_used.UVALUE == 1);
  }

  COMPRESSED ecn_not_present {
    ip_ecn_flags =:= static [ 0 ];
    ENFORCE(ecn_used.UVALUE == 0);
  }
}

rsf_index_enc
{
  UNCOMPRESSED {
    rsf_flag [ 3 ];
  }

  COMPRESSED none {
    rsf_idx  =:= '00' [ 2 ];
    rsf_flag =:= uncompressed_value(3, 0x00);
  }

  COMPRESSED rst_only {
    rsf_idx  =:= '01' [ 2 ];
    rsf_flag =:= uncompressed_value(3, 0x04);
  }

  COMPRESSED syn_only {
    rsf_idx  =:= '10' [ 2 ];
    rsf_flag =:= uncompressed_value(3, 0x02);
  }

  COMPRESSED fin_only {
    rsf_idx  =:= '11' [ 2 ];
    rsf_flag =:= uncompressed_value(3, 0x01);
  }
}

optional_2bit_padding(used_flag)
{
  UNCOMPRESSED {
  }

  COMPRESSED used {
    padding =:= compressed_value(2, 0x0) [ 2 ];
    ENFORCE(used_flag == 1);
  }

  COMPRESSED unused {
    padding =:= compressed_value(0, 0x0);

    ENFORCE(used_flag == 0);
  }
}

// ack_stride_value is the user-selected stride for scaling the
// TCP ack_number
// ip_inner_ecn is the value bound when processing the innermost
// IP header (ipv4 or ipv6 encoding method)
tcp(payload_size, ack_stride_value, ip_inner_ecn)
{
  UNCOMPRESSED {
    src_port      [ 16 ];
    dst_port      [ 16 ];
    seq_number    [ 32 ];
    ack_number    [ 32 ];
    data_offset   [ 4 ];
    tcp_res_flags [ 4 ];
    tcp_ecn_flags [ 2 ];
    urg_flag      [ 1 ];
    ack_flag      [ 1 ];
    psh_flag      [ 1 ];
    rsf_flags     [ 3 ];
    window        [ 16 ];
    checksum      [ 16 ];
    urg_ptr       [ 16 ];
    options       [ (data_offset.UVALUE-5)*32 ];
  }

  CONTROL {
    dummy_field_s =:= field_scaling(payload_size,
      seq_number_scaled.UVALUE, seq_number.UVALUE,
      seq_number_residue.UVALUE) [ 0 ];
    dummy_field_a =:= field_scaling(ack_stride.UVALUE,
      ack_number_scaled.UVALUE, ack_number.UVALUE,
      ack_number_residue.UVALUE) [ 0 ];
    ENFORCE(ack_stride.UVALUE == ack_stride_value);
  }

  INITIAL {
    ack_stride     =:= uncompressed_value(16, 0);
  }

  DEFAULT {
    src_port      =:= static;
    dst_port      =:= static;
    seq_number    =:= static;
    ack_number    =:= static;
    data_offset   =:= inferred_offset;

    tcp_res_flags =:= static;
    tcp_ecn_flags =:= static;
    urg_flag      =:= static;
    ack_flag      =:= uncompressed_value(1, 1);
    rsf_flags     =:= uncompressed_value(3, 0);
    window        =:= static;
    urg_ptr       =:= static;
    ack_stride    =:= static;
    ack_number_scaled =:= static;
    seq_number_scaled =:= static;
    ack_number_residue =:= static;
    seq_number_residue =:= static;
  }

  COMPRESSED tcp_static {
    src_port =:= irregular(16) [ 16 ];
    dst_port =:= irregular(16) [ 16 ];
  }

  COMPRESSED tcp_dynamic {
    ecn_used        =:= one_bit_choice          [ 1 ];
    ack_stride_flag =:= irregular(1)            [ 1 ];
    ack_zero        =:= irregular(1)            [ 1 ];
    urp_zero        =:= irregular(1)            [ 1 ];
    tcp_res_flags   =:= irregular(4)            [ 4 ];
    tcp_ecn_flags   =:= irregular(2)            [ 2 ];
    urg_flag        =:= irregular(1)            [ 1 ];
    ack_flag        =:= irregular(1)            [ 1 ];
    psh_flag        =:= irregular(1)            [ 1 ];
    rsf_flags       =:= irregular(3)            [ 3 ];
    msn             =:= irregular(16)           [ 16 ];
    seq_number      =:= irregular(32)           [ 32 ];
    ack_number      =:=
      zero_or_irreg(ack_zero.CVALUE, 32)        [ 0, 32 ];
    window          =:= irregular(16)           [ 16 ];
    checksum        =:= irregular(16)           [ 16 ];
    urg_ptr         =:=
      zero_or_irreg(urp_zero.CVALUE, 16)        [ 0, 16 ];
    ack_stride      =:=
      static_or_irreg(ack_stride_flag.CVALUE, 16) [ 0, 16 ];
    options         =:= list_tcp_options        [ VARIABLE ];
  }

  COMPRESSED tcp_replicate {
    reserved          =:= '0'                      [ 1 ];
    window_presence   =:= irregular(1)             [ 1 ];
    list_present      =:= irregular(1)             [ 1 ];
    src_port_presence =:= irregular(2)             [ 2 ];

    dst_port_presence =:= irregular(2)             [ 2 ];
    ack_stride_flag   =:= irregular(1)             [ 1 ];
    ack_presence      =:= irregular(1)             [ 1 ];
    urp_presence      =:= irregular(1)             [ 1 ];
    urg_flag          =:= irregular(1)             [ 1 ];
    ack_flag          =:= irregular(1)             [ 1 ];
    psh_flag          =:= irregular(1)             [ 1 ];
    rsf_flags         =:= rsf_index_enc            [ 2 ];
    ecn_used          =:= one_bit_choice           [ 1 ];
    msn               =:= irregular(16)            [ 16 ];
    seq_number        =:= irregular(32)            [ 32 ];
    src_port          =:=
      port_replicate(src_port_presence)      [ 0, 8, 16 ];
    dst_port          =:=
      port_replicate(dst_port_presence)      [ 0, 8, 16 ];
    window            =:=
      static_or_irreg(window_presence, 16)   [ 0, 16 ];
    urg_point         =:=
      static_or_irreg(urp_presence, 16)    [ 0, 16 ];
    ack_number        =:=
      static_or_irreg(ack_presence, 32)    [ 0, 32 ];
    ecn_padding       =:=
      optional_2bit_padding(ecn_used.CVALUE)     [ 0, 2 ];
    tcp_res_flags =:=
      static_or_irreg(ecn_used.CVALUE, 4)        [ 0, 4 ];
    tcp_ecn_flags     =:=
      static_or_irreg(ecn_used.CVALUE, 2)        [ 0, 2 ];
    checksum          =:= irregular(16)            [ 16 ];
    ack_stride        =:=
      static_or_irreg(ack_stride_flag.CVALUE, 16)  [ 0, 16 ];
    options           =:=
      tcp_list_presence_enc(list_present.CVALUE) [ VARIABLE ];
  }

  COMPRESSED tcp_irregular {
    ip_ecn_flags  =:= tcp_irreg_ip_ecn(ip_inner_ecn)  [ 0, 2 ];
    tcp_res_flags =:=
      static_or_irreg(ecn_used.CVALUE, 4)            [ 0, 4 ];
    tcp_ecn_flags =:=
      static_or_irreg(ecn_used.CVALUE, 2)             [ 0, 2 ];
    checksum      =:= irregular(16)                   [ 16 ];
  }
}

///////////////////////////////////////////////////
// Encoding methods used in compressed base headers
///////////////////////////////////////////////////

dscp_enc(flag)
{
  UNCOMPRESSED {
    dscp [ 6 ];
  }

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

  COMPRESSED irreg {
    dscp    =:= irregular(6)           [ 6 ];
    padding =:= compressed_value(2, 0) [ 2 ];
    ENFORCE(flag == 1);
  }
}

ip_id_lsb(behavior, k, p)
{
  UNCOMPRESSED {
    ip_id [ 16 ];
  }

  CONTROL {
    ip_id_nbo    [ 16 ];
  }

  COMPRESSED nbo {
    ip_id_offset =:= lsb(k, p) [ k ];
    ENFORCE(behavior == IP_ID_BEHAVIOR_SEQUENTIAL);
    ENFORCE(ip_id_offset.UVALUE == ip_id.UVALUE - msn.UVALUE);
  }

  COMPRESSED non_nbo {
    ip_id_offset =:= lsb(k, p) [ k ];
    ENFORCE(behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED);
    ENFORCE(ip_id_nbo.UVALUE ==
            (ip_id.UVALUE / 256) + (ip_id.UVALUE % 256) * 256);
    ENFORCE(ip_id_nbo.ULENGTH == 16);
    ENFORCE(ip_id_offset.UVALUE == ip_id_nbo.UVALUE - msn.UVALUE);
  }
}

optional_ip_id_lsb(behavior, indicator)
{
  UNCOMPRESSED {
    ip_id [ 16 ];

  }

  COMPRESSED short {
    ip_id =:= ip_id_lsb(behavior, 8, 3) [ 8 ];
    ENFORCE((behavior == IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    ENFORCE(indicator == 0);
  }

  COMPRESSED long {
    ip_id =:= irregular(16)  [ 16 ];
    ENFORCE((behavior == IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (behavior == IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    ENFORCE(indicator == 1);
    ENFORCE(ip_id_offset.UVALUE == ip_id.UVALUE - msn.UVALUE);
  }

  COMPRESSED not_present {
    ENFORCE((behavior == IP_ID_BEHAVIOR_RANDOM) ||
            (behavior == IP_ID_BEHAVIOR_ZERO));
  }
}
dont_fragment(version)
{
  UNCOMPRESSED {
    df [ 1 ];
  }

  COMPRESSED v4 {
    df =:= irregular(1) [ 1 ];
    ENFORCE(version == 4);
  }

  COMPRESSED v6 {
    df =:= compressed_value(1, 0) [ 1 ];
    ENFORCE(version == 6);
  }
}

//////////////////////////////////
// Actual start of compressed packet formats
// Important note:
//   The base header is the compressed representation
//   of the innermost IP header AND the TCP header.
//////////////////////////////////

// ttl_irregular_chain_flag is set by the user if the TTL/Hop Limit
// of an outer header has changed.  The same value must be passed as

// an argument to the ipv4/ipv6 encoding methods when extracting
// the irregular chain items.
co_baseheader(payload_size, ack_stride_value,
              ttl_irregular_chain_flag, ip_id_behavior_value)
{
  UNCOMPRESSED v4 {
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    version        =:= uncompressed_value(4, 4)        [ 4 ];
    header_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 ];
    next_header                                        [ 8 ];
    checksum                                           [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dest_port                                          [ 16 ];
    seq_number                                         [ 32 ];
    ack_number                                         [ 32 ];
    data_offset                                        [ 4 ];
    tcp_res_flags                                      [ 4 ];
    tcp_ecn_flags                                      [ 2 ];
    urg_flag                                           [ 1 ];
    ack_flag                                           [ 1 ];
    psh_flag                                           [ 1 ];
    rsf_flags                                          [ 3 ];
    window                                             [ 16 ];
    tcp_checksum                                       [ 16 ];
    urg_ptr                                            [ 16 ];
    options                           [ (data_offset.UVALUE-5)*32 ];
  }

  UNCOMPRESSED v6 {
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    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 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dest_port                                          [ 16 ];
    seq_number                                         [ 32 ];
    ack_number                                         [ 32 ];
    data_offset                                        [ 4 ];
    tcp_res_flags                                      [ 4 ];
    tcp_ecn_flags                                      [ 2 ];
    urg_flag                                           [ 1 ];
    ack_flag                                           [ 1 ];
    psh_flag                                           [ 1 ];
    rsf_flags                                          [ 3 ];
    window                                             [ 16 ];
    tcp_checksum                                       [ 16 ];
    urg_ptr                                            [ 16 ];
    options                           [ (data_offset.UVALUE-5)*32 ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    dummy_field_s =:= field_scaling(payload_size,
      seq_number_scaled.UVALUE, seq_number.UVALUE,
      seq_number_residue.UVALUE) [ 0 ];
    dummy_field_a =:= field_scaling(ack_stride.UVALUE,
      ack_number_scaled.UVALUE, ack_number.UVALUE,
      ack_number_residue.UVALUE) [ 0 ];
    ENFORCE(ack_stride.UVALUE == ack_stride_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
  }

  INITIAL {
    ack_stride     =:= uncompressed_value(16, 0);
  }

  DEFAULT {
    tcp_ecn_flags  =:= static;
    data_offset    =:= inferred_offset;
    tcp_res_flags  =:= static;
    rsf_flags      =:= uncompressed_value(3, 0);
    dest_port      =:= static;
    dscp           =:= static;
    src_port       =:= static;
    urg_flag       =:= uncompressed_value(1, 0);

    window         =:= static;
    dest_addr      =:= static;
    version        =:= static;
    ttl_hopl       =:= static;
    src_addr       =:= static;
    df             =:= static;
    ack_number     =:= static;
    urg_ptr        =:= static;
    seq_number     =:= static;
    ack_flag       =:= uncompressed_value(1, 1);
    // The default for "options" is case 2) and 3) from
    // the list in Section 6.3.1 (i.e., nothing present in the
    // baseheader itself).
    payload_length =:= inferred_ip_v6_length;
    checksum       =:= inferred_ip_v4_header_checksum;
    length         =:= inferred_ip_v4_length;
    flow_label     =:= static;
    next_header    =:= static;
    ip_ecn_flags   =:= static;
    // The tcp_checksum has no default,
    // it is considered a part of tcp_irregular
    ip_id_behavior_innermost =:= static;
    ecn_used       =:= static;
    ack_stride    =:= static;
    ack_number_scaled =:= static;
    seq_number_scaled =:= static;
    ack_number_residue =:= static;
    seq_number_residue =:= static;

    // Default is to have no TTL in irregular chain
    // Can only be nonzero if co_common is used
    ENFORCE(ttl_irregular_chain_flag == 0);
  }

  ////////////////////////////////////////////
  // Common compressed packet format
  ////////////////////////////////////////////

  COMPRESSED co_common {
    discriminator        =:= '1111101'                [ 7 ];
    ttl_hopl_outer_flag  =:=
        compressed_value(1, ttl_irregular_chain_flag) [ 1 ];
    ack_flag             =:= irregular(1)             [ 1 ];
    psh_flag             =:= irregular(1)             [ 1 ];
    rsf_flags            =:= rsf_index_enc            [ 2 ];
    msn                  =:= lsb(4, 4)                [ 4 ];
    seq_indicator        =:= irregular(2)             [ 2 ];
    ack_indicator        =:= irregular(2)             [ 2 ];

    ack_stride_indicator =:= irregular(1)             [ 1 ];
    window_indicator     =:= irregular(1)             [ 1 ];
    ip_id_indicator      =:= irregular(1)             [ 1 ];
    urg_ptr_present      =:= irregular(1)             [ 1 ];
    reserved             =:= compressed_value(1, 0)   [ 1 ];
    ecn_used             =:= one_bit_choice           [ 1 ];
    dscp_present         =:= irregular(1)             [ 1 ];
    ttl_hopl_present     =:= irregular(1)             [ 1 ];
    list_present         =:= irregular(1)             [ 1 ];
    ip_id_behavior_innermost       =:= irregular(2)             [ 2 ];
    urg_flag             =:= irregular(1)             [ 1 ];
    df                   =:= dont_fragment(version.UVALUE)   [ 1 ];
    header_crc           =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    seq_number           =:=
      variable_length_32_enc(seq_indicator.CVALUE) [ 0, 8, 16, 32 ];
    ack_number           =:=
      variable_length_32_enc(ack_indicator.CVALUE) [ 0, 8, 16, 32 ];
    ack_stride           =:=
      static_or_irreg(ack_stride_indicator.CVALUE, 16)  [ 0, 16 ];
    window               =:=
      static_or_irreg(window_indicator.CVALUE, 16)      [ 0, 16 ];
    ip_id                =:=
      optional_ip_id_lsb(ip_id_behavior_innermost.UVALUE,
                         ip_id_indicator.CVALUE)      [ 0, 8, 16 ];
    urg_ptr              =:=
      static_or_irreg(urg_ptr_present.CVALUE, 16)     [ 0, 16 ];
    dscp                 =:=
      dscp_enc(dscp_present.CVALUE)                   [ 0, 8 ];
    ttl_hopl             =:=
      static_or_irreg(ttl_hopl_present.CVALUE, 8)     [ 0, 8 ];
    options              =:=
      tcp_list_presence_enc(list_present.CVALUE)      [ VARIABLE ];
  }

  // Send LSBs of sequence number
  COMPRESSED rnd_1 {
    discriminator =:= '101110'                        [ 6 ];
    seq_number    =:= lsb(18, 65535)                  [ 18 ];
    msn           =:= lsb(4, 4)                       [ 4 ];
    psh_flag      =:= irregular(1)                    [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send scaled sequence number LSBs
  COMPRESSED rnd_2 {

    discriminator      =:= '1100'                          [ 4 ];
    seq_number_scaled  =:= lsb(4, 7)                       [ 4 ];
    msn                =:= lsb(4, 4)                       [ 4 ];
    psh_flag           =:= irregular(1)                    [ 1 ];
    header_crc         =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE(payload_size != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send acknowledgment number LSBs
  COMPRESSED rnd_3 {
    discriminator =:= '0'                             [ 1 ];
    ack_number    =:= lsb(15, 8191)                   [ 15 ];
    msn           =:= lsb(4, 4)                       [ 4 ];
    psh_flag      =:= irregular(1)                    [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send acknowledgment number scaled
  COMPRESSED rnd_4 {
    discriminator      =:= '1101'                          [ 4 ];
    ack_number_scaled  =:= lsb(4, 3)                       [ 4 ];
    msn                =:= lsb(4, 4)                       [ 4 ];
    psh_flag           =:= irregular(1)                    [ 1 ];
    header_crc         =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE(ack_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send ACK and sequence number
  COMPRESSED rnd_5 {
    discriminator =:= '100'                           [ 3 ];
    psh_flag      =:= irregular(1)                    [ 1 ];
    msn           =:= lsb(4, 4)                       [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    seq_number    =:= lsb(14, 8191)                   [ 14 ];
    ack_number    =:= lsb(15, 8191)                   [ 15 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send both ACK and scaled sequence number LSBs
  COMPRESSED rnd_6 {
    discriminator      =:= '1010'                          [ 4 ];
    header_crc         =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    psh_flag           =:= irregular(1)                    [ 1 ];
    ack_number         =:= lsb(16, 16383)                  [ 16 ];
    msn                =:= lsb(4, 4)                       [ 4 ];
    seq_number_scaled  =:= lsb(4, 7)                       [ 4 ];
    ENFORCE(payload_size != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send ACK and window
  COMPRESSED rnd_7 {
    discriminator =:= '101111'                        [ 6 ];
    ack_number    =:= lsb(18, 65535)                  [ 18 ];
    window        =:= irregular(16)                   [ 16 ];
    msn           =:= lsb(4, 4)                       [ 4 ];
    psh_flag      =:= irregular(1)                    [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // An extended packet type for seldom-changing fields
  // Can send LSBs of TTL, RSF flags, change ECN behavior, and
  // options list
  COMPRESSED rnd_8 {
    discriminator =:= '10110'                         [ 5 ];
    rsf_flags     =:= rsf_index_enc                   [ 2 ];
    list_present  =:= irregular(1)                    [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    msn           =:= lsb(4, 4)                       [ 4 ];
    psh_flag      =:= irregular(1)                    [ 1 ];
    ttl_hopl      =:= lsb(3, 3)                       [ 3 ];
    ecn_used      =:= one_bit_choice                  [ 1 ];
    seq_number    =:= lsb(16, 65535)                  [ 16 ];
    ack_number    =:= lsb(16, 16383)                  [ 16 ];
    options       =:=
      tcp_list_presence_enc(list_present.CVALUE)      [ VARIABLE ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
  }

  // Send LSBs of sequence number
  COMPRESSED seq_1 {
    discriminator =:= '1010'                                 [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4, 3) [ 4 ];
    seq_number    =:= lsb(16, 32767)                         [ 16 ];
    msn           =:= lsb(4, 4)                              [ 4 ];
    psh_flag      =:= irregular(1)                           [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)        [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send scaled sequence number LSBs
  COMPRESSED seq_2 {
    discriminator      =:= '11010'                         [ 5 ];
    ip_id              =:=
      ip_id_lsb(ip_id_behavior_innermost.UVALUE, 7, 3)     [ 7 ];
    seq_number_scaled  =:= lsb(4, 7)                       [ 4 ];
    msn                =:= lsb(4, 4)                       [ 4 ];
    psh_flag           =:= irregular(1)                    [ 1 ];
    header_crc         =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE(payload_size != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send acknowledgment number LSBs
  COMPRESSED seq_3 {
    discriminator =:= '1001'                                 [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4, 3) [ 4 ];
    ack_number    =:= lsb(16, 16383)                         [ 16 ];
    msn           =:= lsb(4, 4)                              [ 4 ];
    psh_flag      =:= irregular(1)                           [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)        [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send scaled acknowledgment number scaled
  COMPRESSED seq_4 {
    discriminator     =:= '0'                             [ 1 ];
    ack_number_scaled =:= lsb(4, 3)                       [ 4 ];

    // Due to having very few ip_id bits, no negative offset
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 3, 1) [ 3 ];
    msn               =:= lsb(4, 4)                       [ 4 ];
    psh_flag          =:= irregular(1)                    [ 1 ];
    header_crc        =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ENFORCE(ack_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send ACK and sequence number
  COMPRESSED seq_5 {
    discriminator =:= '1000'                                 [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4, 3) [ 4 ];
    ack_number    =:= lsb(16, 16383)                         [ 16 ];
    seq_number    =:= lsb(16, 32767)                         [ 16 ];
    msn           =:= lsb(4, 4)                              [ 4 ];
    psh_flag      =:= irregular(1)                           [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)        [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send both ACK and scaled sequence number LSBs
  COMPRESSED seq_6 {
    discriminator      =:= '11011'                          [ 5 ];
    seq_number_scaled  =:= lsb(4, 7)                        [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 7, 3) [ 7 ];
    ack_number         =:= lsb(16, 16383)                   [ 16 ];
    msn                =:= lsb(4, 4)                        [ 4 ];
    psh_flag           =:= irregular(1)                     [ 1 ];
    header_crc         =:= crc3(THIS.UVALUE, THIS.ULENGTH)  [ 3 ];
    ENFORCE(payload_size != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // Send ACK and window
  COMPRESSED seq_7 {
    discriminator =:= '1100'                                 [ 4 ];
    window        =:= lsb(15, 16383)                         [ 15 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 5, 3) [ 5 ];

    ack_number    =:= lsb(16, 32767)                         [ 16 ];
    msn           =:= lsb(4, 4)                              [ 4 ];
    psh_flag      =:= irregular(1)                           [ 1 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)        [ 3 ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }

  // An extended packet type for seldom-changing fields
  // Can send LSBs of TTL, RSF flags, change ECN behavior, and
  // options list
  COMPRESSED seq_8 {
    discriminator =:= '1011'                                 [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4, 3) [ 4 ];
    list_present  =:= irregular(1)                           [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)        [ 7 ];
    msn           =:= lsb(4, 4)                              [ 4 ];
    psh_flag      =:= irregular(1)                           [ 1 ];
    ttl_hopl      =:= lsb(3, 3)                              [ 3 ];
    ecn_used      =:= one_bit_choice                         [ 1 ];
    ack_number    =:= lsb(15, 8191)                          [ 15 ];
    rsf_flags     =:= rsf_index_enc                          [ 2 ];
    seq_number    =:= lsb(14, 8191)                          [ 14 ];
    options       =:=
      tcp_list_presence_enc(list_present.CVALUE)       [ VARIABLE ];
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
  }
}