Tech-invite3GPPspaceIETFspace
959493929190898887868584838281807978777675747372717069686766656463626160595857565554535251504948474645444342414039383736353433323130292827262524232221201918171615141312111009080706050403020100
in Index   Prev   Next

RFC 5225

RObust Header Compression Version 2 (ROHCv2): Profiles for RTP, UDP, IP, ESP and UDP-Lite

Pages: 124
Proposed Standard
Errata
Part 3 of 4 – Pages 45 to 100
First   Prev   Next

Top   ToC   RFC5225 - Page 45   prevText
6.8.2.4. Header Formats in ROHC-FN
This section defines the complete set of base header formats for ROHCv2 profiles. The base header formats are defined using the ROHC Formal Notation [RFC4997].
Top   ToC   RFC5225 - Page 46
// NOTE: The irregular, static, and dynamic chains (see Section 6.5)
// are defined across multiple encoding methods and are embodied
// in the correspondingly named formats within those encoding
// methods.  In particular, note that the static and dynamic
// chains ordinarily go together.  The uncompressed fields are
// defined across these two formats combined, rather than in one
// or the other of them.  The irregular chain items are likewise
// combined with a baseheader format.

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

// IP-ID behavior constants
IP_ID_BEHAVIOR_SEQUENTIAL         = 0;
IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED = 1;
IP_ID_BEHAVIOR_RANDOM             = 2;
IP_ID_BEHAVIOR_ZERO               = 3;

// UDP-lite checksum coverage behavior constants
UDP_LITE_COVERAGE_INFERRED  = 0;
UDP_LITE_COVERAGE_STATIC    = 1;
UDP_LITE_COVERAGE_IRREGULAR = 2;
// The value 3 is reserved and cannot be used for coverage behavior

// Variable reordering offset
REORDERING_NONE          = 0;
REORDERING_QUARTER       = 1;
REORDERING_HALF          = 2;
REORDERING_THREEQUARTERS = 3;

// Profile names and versions
PROFILE_RTP_0101     = 0x0101;
PROFILE_UDP_0102     = 0x0102;
PROFILE_ESP_0103     = 0x0103;
PROFILE_IP_0104      = 0x0104;
PROFILE_RTP_0107     = 0x0107; // With UDP-LITE
PROFILE_UDPLITE_0108 = 0x0108; // Without RTP

// Default values for RTP timestamp encoding
TS_STRIDE_DEFAULT    = 160;
TIME_STRIDE_DEFAULT  = 0;

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

CONTROL {
Top   ToC   RFC5225 - Page 47
  profile                                    [ 16 ];
  msn                                        [ 16 ];
  reorder_ratio                              [  2 ];
  // ip_id fields are for innermost IP header only
  ip_id_offset                               [ 16 ];
  ip_id_behavior_innermost                   [  2 ];
  // The following are only used in RTP-based profiles
  ts_stride                                  [ 32 ];
  time_stride                                [ 32 ];
  ts_scaled                                  [ 32 ];
  ts_offset                                  [ 32 ];
  // UDP-lite-based profiles only
  coverage_behavior                          [  2 ];
}

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

baseheader_extension_headers       "defined in Section 6.6.1";
baseheader_outer_headers           "defined in Section 6.6.2";
control_crc3_encoding              "defined in Section 6.6.11";
inferred_ip_v4_header_checksum     "defined in Section 6.6.4";
inferred_ip_v4_length              "defined in Section 6.6.6";
inferred_ip_v6_length              "defined in Section 6.6.7";
inferred_mine_header_checksum      "defined in Section 6.6.5";
inferred_scaled_field              "defined in Section 6.6.10";
inferred_sequential_ip_id          "defined in Section 6.6.12";
inferred_udp_length                "defined in Section 6.6.3";
list_csrc(cc_value)                "defined in Section 6.6.13";
timer_based_lsb(time_stride, k, p) "defined in Section 6.6.9";

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

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

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

  COMPRESSED static_enc {
Top   ToC   RFC5225 - Page 48
    ENFORCE(flag == 0);
    field =:= static [ 0 ];
  }
}

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

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

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

// Send the entire value, or keep previous value
sdvl_or_static(flag)
{
  UNCOMPRESSED {
    field [ 32 ];
  }

  COMPRESSED present_7bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^7);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '0' [ 1 ];
    field                 [ 7 ];
  }

  COMPRESSED present_14bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^14);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '10'   [  2 ];
    field                    [ 14 ];
  }

  COMPRESSED present_21bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^21);
Top   ToC   RFC5225 - Page 49
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '110'  [  3 ];
    field                    [ 21 ];
  }

  COMPRESSED present_28bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^28);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '1110'  [  4 ];
    field                     [ 28 ];
  }

  COMPRESSED present_32bit {
    ENFORCE(flag == 1);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '11111111'  [  8 ];
    field                         [ 32 ];
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    field =:= static;
  }
}

// Send the entire value, or revert to default value
sdvl_or_default(flag, default_value)
{
  UNCOMPRESSED {
    field [ 32 ];
  }

  COMPRESSED present_7bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^7);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '0' [ 1 ];
    field                 [ 7 ];
  }

  COMPRESSED present_14bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^14);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '10'   [  2 ];
    field                    [ 14 ];
  }
Top   ToC   RFC5225 - Page 50
  COMPRESSED present_21bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^21);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '110'  [  3 ];
    field                    [ 21 ];
  }

  COMPRESSED present_28bit {
    ENFORCE(flag == 1);
    ENFORCE(field.UVALUE < 2^28);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '1110'  [  4 ];
    field                     [ 28 ];
  }

  COMPRESSED present_32bit {
    ENFORCE(flag == 1);
    ENFORCE(field.CVALUE == field.UVALUE);
    discriminator =:= '11111111'  [  8 ];
    field                         [ 32 ];
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    field =:= uncompressed_value(32, default_value);
  }
}

lsb_7_or_31
{
  UNCOMPRESSED {
    item [ 32 ];
  }

  COMPRESSED lsb_7 {
    discriminator =:= '0'                       [  1 ];
    item          =:= lsb(7, ((2^7) / 4) - 1)   [  7 ];
  }

  COMPRESSED lsb_31 {
    discriminator =:= '1'                       [  1 ];
    item          =:= lsb(31, ((2^31) / 4) - 1) [ 31 ];
  }
}

crc3(data_value, data_length)
{
Top   ToC   RFC5225 - Page 51
  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 ];
  }
}

// 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.
// Does not have an uncompressed side.
field_scaling(stride_value, scaled_value, unscaled_value, residue_value)
{
  UNCOMPRESSED {
    // Nothing
  }

  COMPRESSED no_scaling {
    ENFORCE(stride_value == 0);
    ENFORCE(residue_value == unscaled_value);
    ENFORCE(scaled_value == 0);
  }

  COMPRESSED scaling_used {
    ENFORCE(stride_value != 0);
    ENFORCE(residue_value == (unscaled_value % stride_value));
    ENFORCE(unscaled_value ==
            scaled_value * stride_value + residue_value);
  }
}

////////////////////////////////////////////
// IPv6 Destination options header
////////////////////////////////////////////

ip_dest_opt
{
  UNCOMPRESSED {
Top   ToC   RFC5225 - Page 52
    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_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 ];
  }
Top   ToC   RFC5225 - Page 53
  COMPRESSED hop_opt_dynamic {
    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_irregular {
  }
}

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

optional_lsb_7_or_31(flag)
{
Top   ToC   RFC5225 - Page 54
  UNCOMPRESSED {
    item [ 0, 32 ];
  }

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

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

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

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

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

gre_proto
{
  UNCOMPRESSED {
    protocol [ 16 ];
  }

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

  COMPRESSED ether_v6 {
    discriminator =:= '1'                            [ 1 ];
Top   ToC   RFC5225 - Page 55
    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 {
    ENFORCE((c_flag.UVALUE == 1 && checksum_and_res.ULENGTH == 32)
            || checksum_and_res.ULENGTH == 0);
    ENFORCE((s_flag.UVALUE == 1 && sequence_number.ULENGTH == 32)
            || sequence_number.ULENGTH == 0);
    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      =:= optional_32(k_flag.UVALUE) [ 0, 32 ];
  }

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

  COMPRESSED gre_irregular {
Top   ToC   RFC5225 - Page 56
    checksum_and_res =:= optional_checksum(c_flag.UVALUE) [ 0, 16 ];
    sequence_number  =:=
      optional_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    =:= optional_32(s_bit.UVALUE) [ 0, 32 ];
  }

  COMPRESSED mine_dynamic {
  }

  COMPRESSED mine_irregular {
  }
}

/////////////////////////////////////////////
Top   ToC   RFC5225 - Page 57
// Authentication Header (AH)
/////////////////////////////////////////////

ah
{
  UNCOMPRESSED {
    next_header                            [  8 ];
    length                                 [  8 ];
    res_bits =:= uncompressed_value(16, 0) [ 16 ];
    spi                                    [ 32 ];
    sequence_number                        [ 32 ];
    icv                   [ length.UVALUE*32-32 ];
  }

  DEFAULT {
    next_header     =:= static;
    length          =:= 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 {
    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 {
Top   ToC   RFC5225 - Page 58
    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 ];
  }
}

ipv6(profile_value, is_innermost, outer_ip_flag, reorder_ratio_value)
{
  UNCOMPRESSED {
    version         =:= uncompressed_value(4, 6) [   4 ];
    tos_tc                                       [   8 ];
    flow_label                                   [  20 ];
    payload_length                               [  16 ];
    next_header                                  [   8 ];
    ttl_hopl                                     [   8 ];
    src_addr                                     [ 128 ];
    dst_addr                                     [ 128 ];
  }

  CONTROL {
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(innermost_ip.UVALUE == is_innermost);
    innermost_ip [ 1 ];
  }

  DEFAULT {
    tos_tc         =:= 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 ];
    innermost_ip        =:= irregular(1)     [   1 ];
Top   ToC   RFC5225 - Page 59
    reserved            =:= '0'              [   1 ];
    flow_label          =:= fl_enc           [ 5, 21 ];
    next_header         =:= irregular(8)     [   8 ];
    src_addr            =:= irregular(128)   [ 128 ];
    dst_addr            =:= irregular(128)   [ 128 ];
  }

  COMPRESSED ipv6_endpoint_dynamic {
    ENFORCE((is_innermost == 1) &&
            (profile_value == PROFILE_IP_0104));
    tos_tc        =:= irregular(8)           [  8 ];
    ttl_hopl      =:= irregular(8)           [  8 ];
    reserved      =:= compressed_value(6, 0) [  6 ];
    reorder_ratio =:= irregular(2)           [  2 ];
    msn           =:= irregular(16)          [ 16 ];
  }

  COMPRESSED ipv6_regular_dynamic {
    ENFORCE((is_innermost == 0) ||
            (profile_value != PROFILE_IP_0104));
    tos_tc       =:= irregular(8) [ 8 ];
    ttl_hopl     =:= irregular(8) [ 8 ];
  }

  COMPRESSED ipv6_outer_irregular {
    ENFORCE(is_innermost == 0);
    tos_tc       =:=
        static_or_irreg(outer_ip_flag, 8) [ 0, 8 ];
    ttl_hopl     =:=
        static_or_irreg(outer_ip_flag, 8) [ 0, 8 ];
  }

  COMPRESSED ipv6_innermost_irregular {
    ENFORCE(is_innermost == 1);
  }

}

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

ip_id_enc_dyn(behavior)
{
  UNCOMPRESSED {
    ip_id [ 16 ];
  }
Top   ToC   RFC5225 - Page 60
  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 {
    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 ];
  }
}

ipv4(profile_value, is_innermost, outer_ip_flag, ip_id_behavior_value,
  reorder_ratio_value)
{
  UNCOMPRESSED {
    version     =:= uncompressed_value(4, 4)       [  4 ];
Top   ToC   RFC5225 - Page 61
    hdr_length  =:= uncompressed_value(4, 5)       [  4 ];
    tos_tc                                         [  8 ];
    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(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(innermost_ip.UVALUE == is_innermost);
    ip_id_behavior_outer [ 2 ];
    innermost_ip [ 1 ];
  }

  DEFAULT {
    tos_tc               =:= 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 ];
    innermost_ip        =:= irregular(1)           [  1 ];
    reserved            =:= '000000'               [  6 ];
    protocol            =:= irregular(8)           [  8 ];
    src_addr            =:= irregular(32)          [ 32 ];
    dst_addr            =:= irregular(32)          [ 32 ];
  }

  COMPRESSED ipv4_endpoint_innermost_dynamic {
    ENFORCE((is_innermost == 1) && (profile_value == PROFILE_IP_0104));
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    reserved       =:= '000'                                 [  3 ];
    reorder_ratio  =:= irregular(2)                          [  2 ];
    df             =:= irregular(1)                          [  1 ];
Top   ToC   RFC5225 - Page 62
    ip_id_behavior_innermost =:= irregular(2)                [  2 ];
    tos_tc         =:= irregular(8)                          [  8 ];
    ttl_hopl       =:= irregular(8)                          [  8 ];
    ip_id =:= ip_id_enc_dyn(ip_id_behavior_innermost.UVALUE) [ 0, 16 ];
    msn            =:= irregular(16)                         [ 16 ];
  }

  COMPRESSED ipv4_regular_innermost_dynamic {
    ENFORCE((is_innermost == 1) && (profile_value != PROFILE_IP_0104));
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    reserved       =:= '00000'                               [ 5 ];
    df             =:= irregular(1)                          [ 1 ];
    ip_id_behavior_innermost =:= irregular(2)                [ 2 ];
    tos_tc         =:= irregular(8)                          [ 8 ];
    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 ];
    tos_tc         =:= irregular(8)                        [ 8 ];
    ttl_hopl       =:= irregular(8)                        [ 8 ];
    ip_id =:= ip_id_enc_dyn(ip_id_behavior_outer.UVALUE)   [ 0, 16 ];
  }

  COMPRESSED ipv4_outer_irregular {
    ENFORCE(is_innermost == 0);
    ip_id    =:=
      ip_id_enc_irreg(ip_id_behavior_outer.UVALUE)      [ 0, 16 ];
    tos_tc   =:= static_or_irreg(outer_ip_flag, 8)      [  0, 8 ];
    ttl_hopl =:= static_or_irreg(outer_ip_flag, 8)      [  0, 8 ];
  }

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

}

/////////////////////////////////////////////
// UDP Header
/////////////////////////////////////////////
Top   ToC   RFC5225 - Page 63
udp(profile_value, reorder_ratio_value)
{
  UNCOMPRESSED {
    ENFORCE((profile_value == PROFILE_RTP_0101) ||
            (profile_value == PROFILE_UDP_0102));
    src_port                           [ 16 ];
    dst_port                           [ 16 ];
    udp_length =:= inferred_udp_length [ 16 ];
    checksum                           [ 16 ];
  }

  CONTROL {
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    checksum_used [ 1 ];
  }

  DEFAULT {
    src_port      =:= static;
    dst_port      =:= static;
    checksum_used =:= static;
  }

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

  COMPRESSED udp_endpoint_dynamic {
    ENFORCE(profile_value == PROFILE_UDP_0102);
    ENFORCE(profile == PROFILE_UDP_0102);
    ENFORCE(checksum_used.UVALUE == (checksum.UVALUE != 0));
    checksum      =:= irregular(16)          [ 16 ];
    msn           =:= irregular(16)          [ 16 ];
    reserved      =:= compressed_value(6, 0) [  6 ];
    reorder_ratio =:= irregular(2)           [  2 ];
  }

  COMPRESSED udp_regular_dynamic {
    ENFORCE(profile_value == PROFILE_RTP_0101);
    ENFORCE(checksum_used.UVALUE == (checksum.UVALUE != 0));
    checksum =:= irregular(16) [ 16 ];
  }

  COMPRESSED udp_zero_checksum_irregular {
    ENFORCE(checksum_used.UVALUE == 0);
    checksum =:= uncompressed_value(16, 0)   [ 0 ];
  }
Top   ToC   RFC5225 - Page 64
  COMPRESSED udp_with_checksum_irregular {
    ENFORCE(checksum_used.UVALUE == 1);
    checksum =:= irregular(16) [ 16 ];
  }

}

/////////////////////////////////////////////
// RTP Header
/////////////////////////////////////////////

csrc_list_dynchain(presence, cc_value)
{
  UNCOMPRESSED {
    csrc_list;
  }

  COMPRESSED no_list {
    ENFORCE(cc_value == 0);
    ENFORCE(presence == 0);
    csrc_list =:= uncompressed_value(0, 0) [ 0 ];
  }

  COMPRESSED list_present {
    ENFORCE(presence == 1);
    csrc_list =:= list_csrc(cc_value) [ VARIABLE ];
  }
}

rtp(profile_value, ts_stride_value, time_stride_value,
    reorder_ratio_value)
{
  UNCOMPRESSED {
    ENFORCE((profile_value == PROFILE_RTP_0101) ||
            (profile_value == PROFILE_RTP_0107));
    rtp_version =:= uncompressed_value(2, 0) [  2 ];
    pad_bit                                  [  1 ];
    extension                                [  1 ];
    cc                                       [  4 ];
    marker                                   [  1 ];
    payload_type                             [  7 ];
    sequence_number                          [ 16 ];
    timestamp                                [ 32 ];
    ssrc                                     [ 32 ];
    csrc_list                                [ cc.UVALUE * 32 ];
  }

  CONTROL {
Top   ToC   RFC5225 - Page 65
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(time_stride_value == time_stride.UVALUE);
    ENFORCE(ts_stride_value == ts_stride.UVALUE);
    dummy_field =:= field_scaling(ts_stride.UVALUE,
      ts_scaled.UVALUE, timestamp.UVALUE, ts_offset.UVALUE) [ 0 ];
  }

  INITIAL {
    ts_stride     =:= uncompressed_value(32, TS_STRIDE_DEFAULT);
    time_stride   =:= uncompressed_value(32, TIME_STRIDE_DEFAULT);
  }

  DEFAULT {
    ENFORCE(msn.UVALUE == sequence_number.UVALUE);
    pad_bit         =:= static;
    extension       =:= static;
    cc              =:= static;
    marker          =:= static;
    payload_type    =:= static;
    sequence_number =:= static;
    timestamp       =:= static;
    ssrc            =:= static;
    csrc_list       =:= static;
    ts_stride       =:= static;
    time_stride     =:= static;
    ts_scaled       =:= static;
    ts_offset       =:= static;
  }

  COMPRESSED rtp_static {
    ssrc            =:= irregular(32)  [ 32 ];
  }

  COMPRESSED rtp_dynamic {
    reserved        =:= compressed_value(1, 0)       [  1 ];
    reorder_ratio   =:= irregular(2)                 [  2 ];
    list_present    =:= irregular(1)                 [  1 ];
    tss_indicator   =:= irregular(1)                 [  1 ];
    tis_indicator   =:= irregular(1)                 [  1 ];
    pad_bit         =:= irregular(1)                 [  1 ];
    extension       =:= irregular(1)                 [  1 ];
    marker          =:= irregular(1)                 [  1 ];
    payload_type    =:= irregular(7)                 [  7 ];
    sequence_number =:= irregular(16)                [ 16 ];
    timestamp       =:= irregular(32)                [ 32 ];
    ts_stride       =:= sdvl_or_default(tss_indicator.CVALUE,
      TS_STRIDE_DEFAULT)                             [ VARIABLE ];
Top   ToC   RFC5225 - Page 66
    time_stride     =:= sdvl_or_default(tis_indicator.CVALUE,
      TIME_STRIDE_DEFAULT)                           [ VARIABLE ];
    csrc_list   =:= csrc_list_dynchain(list_present.CVALUE,
      cc.UVALUE)                                     [ VARIABLE ];
  }

  COMPRESSED rtp_irregular {
  }
}

/////////////////////////////////////////////
// UDP-Lite Header
/////////////////////////////////////////////

checksum_coverage_dynchain(behavior)
{
  UNCOMPRESSED {
    checksum_coverage [ 16 ];
  }

  COMPRESSED inferred_coverage {
    ENFORCE(behavior == UDP_LITE_COVERAGE_INFERRED);
    checksum_coverage =:= inferred_udp_length [  0 ];
  }

  COMPRESSED static_coverage {
    ENFORCE(behavior == UDP_LITE_COVERAGE_STATIC);
    checksum_coverage =:= irregular(16)       [ 16 ];
  }

  COMPRESSED irregular_coverage {
    ENFORCE(behavior == UDP_LITE_COVERAGE_IRREGULAR);
    checksum_coverage =:= irregular(16)       [ 16 ];
  }
}

checksum_coverage_irregular(behavior)
{
  UNCOMPRESSED {
    checksum_coverage [ 16 ];
  }

  COMPRESSED inferred_coverage {
    ENFORCE(behavior == UDP_LITE_COVERAGE_INFERRED);
    checksum_coverage =:= inferred_udp_length [  0 ];
  }

  COMPRESSED static_coverage {
Top   ToC   RFC5225 - Page 67
    ENFORCE(behavior == UDP_LITE_COVERAGE_STATIC);
    checksum_coverage =:= static              [  0 ];
  }

  COMPRESSED irregular_coverage {
    ENFORCE(behavior == UDP_LITE_COVERAGE_IRREGULAR);
    checksum_coverage =:= irregular(16)       [ 16 ];
  }
}

udp_lite(profile_value, reorder_ratio_value, coverage_behavior_value)
{
  UNCOMPRESSED {
    ENFORCE((profile_value == PROFILE_RTP_0107) ||
            (profile_value == PROFILE_UDPLITE_0108));
    src_port          [ 16 ];
    dst_port          [ 16 ];
    checksum_coverage [ 16 ];
    checksum          [ 16 ];
  }

  CONTROL {
    ENFORCE(profile == profile_value);
    ENFORCE(coverage_behavior.UVALUE == coverage_behavior_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
  }

  DEFAULT {
    src_port          =:= static;
    dst_port          =:= static;
    coverage_behavior =:= static;
  }

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

  COMPRESSED udp_lite_endpoint_dynamic {
    ENFORCE(profile_value == PROFILE_UDPLITE_0108);
    reserved =:= compressed_value(4, 0)                      [  4 ];
    coverage_behavior =:= irregular(2)                       [  2 ];
    reorder_ratio     =:= irregular(2)                       [  2 ];
    checksum_coverage =:=
      checksum_coverage_dynchain(coverage_behavior.UVALUE)   [ 16 ];
    checksum          =:= irregular(16)                      [ 16 ];
    msn               =:= irregular(16)                      [ 16 ];
  }
Top   ToC   RFC5225 - Page 68
  COMPRESSED udp_lite_regular_dynamic {
    ENFORCE(profile_value == PROFILE_RTP_0107);
    coverage_behavior =:= irregular(2)                       [  2 ];
    reserved =:= compressed_value(6, 0)                      [  6 ];
    checksum_coverage =:=
        checksum_coverage_dynchain(coverage_behavior.UVALUE) [ 16 ];
    checksum =:= irregular(16)                               [ 16 ];
  }

  COMPRESSED udp_lite_irregular {
    checksum_coverage =:=
      checksum_coverage_irregular(coverage_behavior.UVALUE) [ 0, 16 ];
    checksum          =:= irregular(16)                     [ 16 ];
  }
}

/////////////////////////////////////////////
// ESP Header
/////////////////////////////////////////////

esp(profile_value, reorder_ratio_value)
{
  UNCOMPRESSED {
    ENFORCE(profile_value == PROFILE_ESP_0103);
    ENFORCE(msn.UVALUE == sequence_number.UVALUE % 65536);
    spi             [ 32 ];
    sequence_number [ 32 ];
  }

  CONTROL {
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
  }

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

  COMPRESSED esp_static {
    spi =:= irregular(32)                         [ 32 ];
  }

  COMPRESSED esp_dynamic {
    sequence_number =:= irregular(32)             [ 32 ];
    reserved        =:= compressed_value(6, 0)    [  6 ];
    reorder_ratio   =:= irregular(2)              [  2 ];
  }
Top   ToC   RFC5225 - Page 69
  COMPRESSED esp_irregular {
  }
}

///////////////////////////////////////////////////
// Encoding methods used in the profiles' CO headers
///////////////////////////////////////////////////

// Variable reordering offset used for MSN
msn_lsb(k)
{
  UNCOMPRESSED {
    master [ VARIABLE ];
  }

  COMPRESSED none {
    ENFORCE(reorder_ratio.UVALUE == REORDERING_NONE);
    master =:= lsb(k, 1);
  }

  COMPRESSED quarter {
    ENFORCE(reorder_ratio.UVALUE == REORDERING_QUARTER);
    master =:= lsb(k, ((2^k) / 4) - 1);
  }

  COMPRESSED half {
    ENFORCE(reorder_ratio.UVALUE == REORDERING_HALF);
    master =:= lsb(k, ((2^k) / 2) - 1);
  }

  COMPRESSED threequarters {
    ENFORCE(reorder_ratio.UVALUE == REORDERING_THREEQUARTERS);
    master =:= lsb(k, (((2^k) * 3) / 4) - 1);
  }
}

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

  CONTROL {
    ip_id_nbo    [ 16 ];
  }

  COMPRESSED nbo {
    ENFORCE(behavior == IP_ID_BEHAVIOR_SEQUENTIAL);
Top   ToC   RFC5225 - Page 70
    ENFORCE(ip_id_offset.UVALUE == ip_id.UVALUE - msn.UVALUE);
    ip_id_offset =:= lsb(k, ((2^k) / 4) - 1) [ k ];
  }

  COMPRESSED non_nbo {
    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);
    ip_id_offset =:= lsb(k, ((2^k) / 4) - 1) [ k ];
  }
}

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

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

  COMPRESSED long {
    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);
    ip_id =:= irregular(16)  [ 16 ];
  }

  COMPRESSED not_present {
    ENFORCE((behavior == IP_ID_BEHAVIOR_RANDOM) ||
            (behavior == IP_ID_BEHAVIOR_ZERO));
  }
}

dont_fragment(version)
{
  UNCOMPRESSED {
    df [ 0, 1 ];
  }

  COMPRESSED v4 {
Top   ToC   RFC5225 - Page 71
    ENFORCE(version == 4);
    df =:= irregular(1) [ 1 ];
  }

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

pt_irr_or_static(flag)
{
  UNCOMPRESSED {
    payload_type [ 7 ];
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    payload_type =:= static [ 0 ];
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    reserved     =:= compressed_value(1, 0) [ 1 ];
    payload_type =:= irregular(7)           [ 7 ];
  }
}

csrc_list_presence(presence, cc_value)
{
  UNCOMPRESSED {
    csrc_list;
  }

  COMPRESSED no_list {
    ENFORCE(presence == 0);
    csrc_list =:= static [ 0 ];
  }

  COMPRESSED list_present {
    ENFORCE(presence == 1);
    csrc_list =:= list_csrc(cc_value) [ VARIABLE ];
  }
}

scaled_ts_lsb(time_stride_value, k)
{
  UNCOMPRESSED {
Top   ToC   RFC5225 - Page 72
    timestamp [ 32 ];
  }

  COMPRESSED timerbased {
    ENFORCE(time_stride_value != 0);
    timestamp =:= timer_based_lsb(time_stride_value, k,
                                  ((2^k) / 2) - 1);
  }

  COMPRESSED regular {
    ENFORCE(time_stride_value == 0);
    timestamp =:= lsb(k, ((2^k) / 4) - 1);
  }
}

// Self-describing variable length encoding with reordering offset
sdvl_sn_lsb(field_width)
{
  UNCOMPRESSED {
    field [ field_width ];
  }

  COMPRESSED lsb7 {
    discriminator =:= '0'   [ 1 ];
    field =:= msn_lsb(7)    [ 7 ];
  }

  COMPRESSED lsb14 {
    discriminator =:= '10'  [  2 ];
    field =:= msn_lsb(14)   [ 14 ];
  }

  COMPRESSED lsb21 {
    discriminator =:= '110'  [  3 ];
    field =:= msn_lsb(21)    [ 21 ];
  }

  COMPRESSED lsb28 {
    discriminator =:= '1110' [  4 ];
    field =:= msn_lsb(28)    [ 28 ];
  }

  COMPRESSED lsb32 {
    discriminator =:= '11111111'        [  8 ];
    field =:= irregular(field_width)    [ field_width ];
  }
}
Top   ToC   RFC5225 - Page 73
// Self-describing variable length encoding
sdvl_lsb(field_width)
{
  UNCOMPRESSED {
    field [ field_width ];
  }

  COMPRESSED lsb7 {
    discriminator =:= '0'               [ 1 ];
    field =:= lsb(7, ((2^7) / 4) - 1)   [ 7 ];
  }

  COMPRESSED lsb14 {
    discriminator =:= '10'              [  2 ];
    field =:= lsb(14, ((2^14) / 4) - 1) [ 14 ];
  }

  COMPRESSED lsb21 {
    discriminator =:= '110'             [  3 ];
    field =:= lsb(21, ((2^21) / 4) - 1) [ 21 ];
  }

  COMPRESSED lsb28 {
    discriminator =:= '1110'            [  4 ];
    field =:= lsb(28, ((2^28) / 4) - 1) [ 28 ];
  }

  COMPRESSED lsb32 {
    discriminator =:= '11111111'        [  8 ];
    field =:= irregular(field_width)    [ field_width ];
  }
}

sdvl_scaled_ts_lsb(time_stride)
{
   UNCOMPRESSED {
     field [ 32 ];
   }

   COMPRESSED lsb7 {
     discriminator =:= '0'                     [  1 ];
     field =:= scaled_ts_lsb(time_stride, 7)   [  7 ];
   }

   COMPRESSED lsb14 {
     discriminator =:= '10'                    [  2 ];
     field =:= scaled_ts_lsb(time_stride, 14)  [ 14 ];
   }
Top   ToC   RFC5225 - Page 74
   COMPRESSED lsb21 {
     discriminator =:= '110'                   [  3 ];
     field =:= scaled_ts_lsb(time_stride, 21)  [ 21 ];
   }

   COMPRESSED lsb28 {
     discriminator =:= '1110'                  [  4 ];
     field =:= scaled_ts_lsb(time_stride, 28)  [ 28 ];
   }

   COMPRESSED lsb32 {
     discriminator =:= '11111111'              [  8 ];
     field =:= irregular(32)                   [ 32 ];
   }
}

variable_scaled_timestamp(tss_flag, tsc_flag, ts_stride, time_stride)
{
  UNCOMPRESSED {
    scaled_value [ 32 ];
  }

  COMPRESSED present {
    ENFORCE((tss_flag == 0) && (tsc_flag == 1));
    ENFORCE(ts_stride != 0);
    scaled_value =:= sdvl_scaled_ts_lsb(time_stride) [ VARIABLE ];
  }

  COMPRESSED not_present {
    ENFORCE(((tss_flag == 1) && (tsc_flag == 0)) ||
            ((tss_flag == 0) && (tsc_flag == 0)));
  }
}

variable_unscaled_timestamp(tss_flag, tsc_flag)
{
  UNCOMPRESSED {
    timestamp [ 32 ];
  }

  COMPRESSED present {
    ENFORCE(((tss_flag == 1) && (tsc_flag == 0)) ||
            ((tss_flag == 0) && (tsc_flag == 0)));
    timestamp =:= sdvl_lsb(32);
  }

  COMPRESSED not_present {
    ENFORCE((tss_flag == 0) && (tsc_flag == 1));
Top   ToC   RFC5225 - Page 75
  }
}

profile_1_7_flags1_enc(flag, ip_version)
{
  UNCOMPRESSED {
    ip_outer_indicator  [ 1 ];
    ttl_hopl_indicator  [ 1 ];
    tos_tc_indicator    [ 1 ];
    df                  [ 0, 1 ];
    ip_id_behavior      [ 2 ];
    reorder_ratio       [ 2 ];
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    ENFORCE(ip_outer_indicator.CVALUE == 0);
    ENFORCE(ttl_hopl_indicator.CVALUE == 0);
    ENFORCE(tos_tc_indicator.CVALUE == 0);
    df                   =:= static;
    ip_id_behavior       =:= static;
    reorder_ratio        =:= static;
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    ip_outer_indicator  =:= irregular(1)                [ 1 ];
    ttl_hopl_indicator  =:= irregular(1)                [ 1 ];
    tos_tc_indicator    =:= irregular(1)                [ 1 ];
    df                  =:= dont_fragment(ip_version)   [ 1 ];
    ip_id_behavior      =:= irregular(2)                [ 2 ];
    reorder_ratio       =:= irregular(2)                [ 2 ];
  }
}

profile_1_flags2_enc(flag)
{
  UNCOMPRESSED {
    list_indicator        [ 1 ];
    pt_indicator          [ 1 ];
    time_stride_indicator [ 1 ];
    pad_bit               [ 1 ];
    extension             [ 1 ];
  }

  COMPRESSED not_present{
    ENFORCE(flag == 0);
    ENFORCE(list_indicator.UVALUE == 0);
Top   ToC   RFC5225 - Page 76
    ENFORCE(pt_indicator.UVALUE == 0);
    ENFORCE(time_stride_indicator.UVALUE == 0);
    pad_bit      =:= static;
    extension    =:= static;
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    list_indicator =:= irregular(1)                  [ 1 ];
    pt_indicator   =:= irregular(1)                  [ 1 ];
    time_stride_indicator =:= irregular(1)           [ 1 ];
    pad_bit        =:= irregular(1)                  [ 1 ];
    extension      =:= irregular(1)                  [ 1 ];
    reserved       =:= compressed_value(3, 0)        [ 3 ];
  }
}

profile_2_3_4_flags_enc(flag, ip_version)
{
  UNCOMPRESSED {
    ip_outer_indicator [ 1 ];
    df                 [ 0, 1 ];
    ip_id_behavior     [ 2 ];
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    ENFORCE(ip_outer_indicator.CVALUE == 0);
    df                 =:= static;
    ip_id_behavior     =:= static;
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    ip_outer_indicator =:= irregular(1)              [ 1 ];
    df                 =:= dont_fragment(ip_version) [ 1 ];
    ip_id_behavior     =:= irregular(2)              [ 2 ];
    reserved           =:= compressed_value(4, 0)    [ 4 ];
  }
}

profile_8_flags_enc(flag, ip_version)
{
  UNCOMPRESSED {
    ip_outer_indicator  [ 1 ];
    df                  [ 0, 1 ];
    ip_id_behavior      [ 2 ];
    coverage_behavior   [ 2 ];
Top   ToC   RFC5225 - Page 77
  }

  COMPRESSED not_present {
    ENFORCE(flag == 0);
    ENFORCE(ip_outer_indicator.CVALUE == 0);
    df                  =:= static;
    ip_id_behavior      =:= static;
    coverage_behavior   =:= static;
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    reserved            =:= compressed_value(2, 0)      [ 2 ];
    ip_outer_indicator  =:= irregular(1)                [ 1 ];
    df                  =:= dont_fragment(ip_version)   [ 1 ];
    ip_id_behavior      =:= irregular(2)                [ 2 ];
    coverage_behavior   =:= irregular(2)                [ 2 ];
  }
}

profile_7_flags2_enc(flag)
{
  UNCOMPRESSED {
    list_indicator          [ 1 ];
    pt_indicator            [ 1 ];
    time_stride_indicator   [ 1 ];
    pad_bit                 [ 1 ];
    extension               [ 1 ];
    coverage_behavior       [ 2 ];
  }

  COMPRESSED not_present{
    ENFORCE(flag == 0);
    ENFORCE(list_indicator.CVALUE == 0);
    ENFORCE(pt_indicator.CVALUE == 0);
    ENFORCE(time_stride_indicator.CVALUE == 0);
    pad_bit             =:= static;
    extension           =:= static;
    coverage_behavior   =:= static;
  }

  COMPRESSED present {
    ENFORCE(flag == 1);
    reserved       =:= compressed_value(1, 0)      [ 1 ];
    list_indicator =:= irregular(1)                [ 1 ];
    pt_indicator   =:= irregular(1)                [ 1 ];
    time_stride_indicator =:= irregular(1)         [ 1 ];
    pad_bit        =:= irregular(1)                [ 1 ];
Top   ToC   RFC5225 - Page 78
    extension      =:= irregular(1)                [ 1 ];
    coverage_behavior =:= irregular(2)             [ 2 ];
  }
}

////////////////////////////////////////////
// RTP profile
////////////////////////////////////////////

rtp_baseheader(profile_value, ts_stride_value, time_stride_value,
               outer_ip_flag, ip_id_behavior_value,
               reorder_ratio_value)
{
  UNCOMPRESSED v4 {
    ENFORCE(msn.UVALUE == sequence_number.UVALUE);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
    tos_tc                                             [  8 ];
    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 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dst_port                                           [ 16 ];
    udp_length  =:= inferred_udp_length                [ 16 ];
    udp_checksum                                       [ 16 ];
    rtp_version =:= uncompressed_value(2, 2)           [  2 ];
    pad_bit                                            [  1 ];
    extension                                          [  1 ];
    cc                                                 [  4 ];
    marker                                             [  1 ];
    payload_type                                       [  7 ];
    sequence_number                                    [ 16 ];
    timestamp                                          [ 32 ];
    ssrc                                               [ 32 ];
    csrc_list                                          [ VARIABLE ];
  }

  UNCOMPRESSED v6 {
Top   ToC   RFC5225 - Page 79
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    ENFORCE(msn.UVALUE == sequence_number.UVALUE);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 6)        [   4 ];
    tos_tc                                             [   8 ];
    flow_label                                         [  20 ];
    payload_length =:= inferred_ip_v6_length           [  16 ];
    next_header                                        [   8 ];
    ttl_hopl                                           [   8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [  16 ];
    dst_port                                           [  16 ];
    udp_length     =:= inferred_udp_length             [  16 ];
    udp_checksum                                       [  16 ];
    rtp_version    =:= uncompressed_value(2, 2)        [   2 ];
    pad_bit                                            [   1 ];
    extension                                          [   1 ];
    cc                                                 [   4 ];
    marker                                             [   1 ];
    payload_type                                       [   7 ];
    sequence_number                                    [  16 ];
    timestamp                                          [  32 ];
    ssrc                                               [  32 ];
    csrc_list                                          [ VARIABLE ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_RTP_0101);
    ENFORCE(profile == profile_value);
    ENFORCE(time_stride.UVALUE == time_stride_value);
    ENFORCE(ts_stride.UVALUE == ts_stride_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    dummy_field =:= field_scaling(ts_stride.UVALUE,
      ts_scaled.UVALUE, timestamp.UVALUE, ts_offset.UVALUE) [ 0 ];
  }

  INITIAL {
    ts_stride     =:= uncompressed_value(32, TS_STRIDE_DEFAULT);
    time_stride   =:= uncompressed_value(32, TIME_STRIDE_DEFAULT);
  }

  DEFAULT {
    ENFORCE(outer_ip_flag == 0);
Top   ToC   RFC5225 - Page 80
    tos_tc          =:= static;
    dest_addr       =:= static;
    ttl_hopl        =:= static;
    src_addr        =:= static;
    df              =:= static;
    flow_label      =:= static;
    next_header     =:= static;
    src_port        =:= static;
    dst_port        =:= static;
    pad_bit         =:= static;
    extension       =:= static;
    cc              =:= static;
    // When marker not present in packets, it is assumed 0
    marker          =:= uncompressed_value(1, 0);
    payload_type    =:= static;
    sequence_number =:= static;
    timestamp       =:= static;
    ssrc            =:= static;
    csrc_list       =:= static;
    ts_stride       =:= static;
    time_stride     =:= static;
    ts_scaled       =:= static;
    ts_offset       =:= static;
    reorder_ratio   =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    marker               =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags1_indicator     =:= irregular(1)                  [ 1 ];
    flags2_indicator     =:= irregular(1)                  [ 1 ];
    tsc_indicator        =:= irregular(1)                  [ 1 ];
    tss_indicator        =:= irregular(1)                  [ 1 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];

    outer_ip_indicator : ttl_hopl_indicator :
      tos_tc_indicator : df : ip_id_behavior_innermost : reorder_ratio
      =:= profile_1_7_flags1_enc(flags1_indicator.CVALUE,
        ip_version.UVALUE)                                 [ 0, 8 ];
    list_indicator : pt_indicator : tis_indicator : pad_bit :
      extension =:= profile_1_flags2_enc(
        flags2_indicator.CVALUE)                           [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
Top   ToC   RFC5225 - Page 81
    ttl_hopl =:= static_or_irreg(ttl_hopl_indicator.CVALUE,
      ttl_hopl.ULENGTH)                                    [ 0, 8 ];
    payload_type =:= pt_irr_or_static(pt_indicator)        [ 0, 8 ];
    sequence_number =:=
      sdvl_sn_lsb(sequence_number.ULENGTH)                [ VARIABLE ];
    ip_id =:= ip_id_sequential_variable(
      ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE) [ 0, 8, 16 ];
    ts_scaled =:= variable_scaled_timestamp(tss_indicator.CVALUE,
      tsc_indicator.CVALUE, ts_stride.UVALUE,
      time_stride.UVALUE)                                 [ VARIABLE ];
    timestamp =:= variable_unscaled_timestamp(tss_indicator.CVALUE,
      tsc_indicator.CVALUE)                               [ VARIABLE ];
    ts_stride =:= sdvl_or_static(tss_indicator.CVALUE)    [ VARIABLE ];
    time_stride =:= sdvl_or_static(tis_indicator.CVALUE)  [ VARIABLE ];
    csrc_list =:= csrc_list_presence(list_indicator.CVALUE,
      cc.UVALUE)                                          [ VARIABLE ];
  }

  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator =:= '0'                             [ 1 ];
    msn           =:= msn_lsb(4)                      [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    timestamp     =:= inferred_scaled_field           [ 0 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
    discriminator =:= '1000'                          [ 4 ];
    msn           =:= msn_lsb(5)                      [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    timestamp     =:= inferred_scaled_field           [ 0 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1 replacement
  COMPRESSED pt_1_rnd {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
    discriminator =:= '101'                                [ 3 ];
    marker        =:= irregular(1)                         [ 1 ];
    msn           =:= msn_lsb(4)                           [ 4 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)      [ 3 ];
Top   ToC   RFC5225 - Page 82
  }

  // UO-1-ID replacement
  COMPRESSED pt_1_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '1001'                                [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
    msn           =:= msn_lsb(5)                            [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)       [ 3 ];
    timestamp     =:= inferred_scaled_field                 [ 0 ];
  }

  // UO-1-TS replacement
  COMPRESSED pt_1_seq_ts {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '101'                                [ 3 ];
    marker        =:= irregular(1)                         [ 1 ];
    msn           =:= msn_lsb(4)                           [ 4 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)      [ 3 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UOR-2 replacement
  COMPRESSED pt_2_rnd {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
    discriminator =:= '110'                                [ 3 ];
    msn           =:= msn_lsb(7)                           [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 6) [ 6 ];
    marker        =:= irregular(1)                         [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)      [ 7 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
Top   ToC   RFC5225 - Page 83
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '11000'                               [ 5 ];
    msn           =:= msn_lsb(7)                            [ 7 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 5) [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    timestamp     =:= inferred_scaled_field                 [ 0 ];
  }

  // UOR-2-ID-ext1 replacement (both TS and IP-ID)
  COMPRESSED pt_2_seq_both {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '11001'                               [ 5 ];
    msn           =:= msn_lsb(7)                            [ 7 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 5) [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 7)  [ 7 ];
    marker        =:= irregular(1)                          [ 1 ];
  }

  // UOR-2-TS replacement
  COMPRESSED pt_2_seq_ts {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '1101'                               [ 4 ];
    msn           =:= msn_lsb(7)                           [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    marker        =:= irregular(1)                         [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)      [ 7 ];
    ip_id         =:= inferred_sequential_ip_id            [ 0 ];
  }
}

////////////////////////////////////////////
// UDP profile
////////////////////////////////////////////

udp_baseheader(profile_value, outer_ip_flag, ip_id_behavior_value,
               reorder_ratio_value)
{
  UNCOMPRESSED v4 {
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
Top   ToC   RFC5225 - Page 84
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
    tos_tc                                             [  8 ];
    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 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dst_port                                           [ 16 ];
    udp_length     =:= inferred_udp_length             [ 16 ];
    udp_checksum                                       [ 16 ];
  }

  UNCOMPRESSED v6 {
    ENFORCE(ip_id_behavior.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 6)        [  4 ];
    tos_tc                                             [  8 ];
    flow_label                                         [ 20 ];
    payload_length =:= inferred_ip_v6_length           [ 16 ];
    next_header                                        [  8 ];
    ttl_hopl                                           [  8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dst_port                                           [ 16 ];
    udp_length     =:= inferred_udp_length             [ 16 ];
    udp_checksum                                       [ 16 ];
    df    =:= uncompressed_value(0,0)                  [  0 ];
    ip_id =:= uncompressed_value(0,0)                  [  0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_UDP_0102);
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
  }
Top   ToC   RFC5225 - Page 85
  DEFAULT {
    ENFORCE(outer_ip_flag == 0);
    tos_tc         =:= static;
    dest_addr      =:= static;
    ip_version     =:= static;
    ttl_hopl       =:= static;
    src_addr       =:= static;
    df             =:= static;
    flow_label     =:= static;
    next_header    =:= static;
    src_port       =:= static;
    dst_port       =:= static;
    reorder_ratio  =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags_indicator      =:= irregular(1)                  [ 1 ];
    ttl_hopl_indicator   =:= irregular(1)                  [ 1 ];
    tos_tc_indicator     =:= irregular(1)                  [ 1 ];
    reorder_ratio        =:= irregular(2)                  [ 2 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];
    outer_ip_indicator : df : ip_id_behavior_innermost =:=
      profile_2_3_4_flags_enc(
      flags_indicator.CVALUE, ip_version.UVALUE)           [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
    ttl_hopl =:= static_or_irreg(ttl_hopl_indicator.CVALUE,
      ttl_hopl.ULENGTH)                                    [ 0, 8 ];
    msn                  =:= msn_lsb(8)                    [ 8 ];
    ip_id =:= ip_id_sequential_variable(ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE)                          [ 0, 8, 16 ];
  }

  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator =:= '0'                             [ 1 ];
    msn           =:= msn_lsb(4)                      [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
Top   ToC   RFC5225 - Page 86
    discriminator =:= '100'                           [ 3 ];
    msn           =:= msn_lsb(6)                      [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1-ID replacement (PT-1 only used for sequential)
  COMPRESSED pt_1_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '101'                                 [ 3 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)       [ 3 ];
    msn           =:= msn_lsb(6)                            [ 6 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '110'                                 [ 3 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 6) [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    msn           =:= msn_lsb(8)                            [ 8 ];
  }
}

////////////////////////////////////////////
// ESP profile
////////////////////////////////////////////

esp_baseheader(profile_value, outer_ip_flag, ip_id_behavior_value,
               reorder_ratio_value)
{
  UNCOMPRESSED v4 {
    ENFORCE(msn.UVALUE == sequence_number.UVALUE % 65536);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
    tos_tc                                             [  8 ];
    length         =:= inferred_ip_v4_length           [ 16 ];
    ip_id                                              [ 16 ];
    rf             =:= uncompressed_value(1, 0)        [  1 ];
    df                                                 [  1 ];
Top   ToC   RFC5225 - Page 87
    mf             =:= uncompressed_value(1, 0)        [  1 ];
    frag_offset    =:= uncompressed_value(13, 0)       [ 13 ];
    ttl_hopl                                           [  8 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    spi                                                [ 32 ];
    sequence_number                                    [ 32 ];
  }

  UNCOMPRESSED v6 {
    ENFORCE(msn.UVALUE == (sequence_number.UVALUE % 65536));
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 6)        [   4 ];
    tos_tc                                             [   8 ];
    flow_label                                         [  20 ];
    payload_length =:= inferred_ip_v6_length           [  16 ];
    next_header                                        [   8 ];
    ttl_hopl                                           [   8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    spi                                                [  32 ];
    sequence_number                                    [  32 ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_ESP_0103);
    ENFORCE(profile == profile_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
  }

  DEFAULT {
    ENFORCE(outer_ip_flag == 0);
    tos_tc          =:= static;
    dest_addr       =:= static;
    ttl_hopl        =:= static;
    src_addr        =:= static;
    df              =:= static;
    flow_label      =:= static;
    next_header     =:= static;
    spi             =:= static;
Top   ToC   RFC5225 - Page 88
    sequence_number =:= static;
    reorder_ratio   =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags_indicator      =:= irregular(1)                  [ 1 ];
    ttl_hopl_indicator   =:= irregular(1)                  [ 1 ];
    tos_tc_indicator     =:= irregular(1)                  [ 1 ];
    reorder_ratio        =:= irregular(2)                  [ 2 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];

    outer_ip_indicator : df : ip_id_behavior_innermost =:=
      profile_2_3_4_flags_enc(
      flags_indicator.CVALUE, ip_version.UVALUE)           [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
    ttl_hopl =:= static_or_irreg(ttl_hopl_indicator.CVALUE,
      ttl_hopl.ULENGTH)                                    [ 0, 8 ];
    sequence_number =:=
      sdvl_sn_lsb(sequence_number.ULENGTH)             [ VARIABLE ];
    ip_id =:= ip_id_sequential_variable(ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE)                          [ 0, 8, 16 ];
  }

  // Sequence number sent instead of MSN due to field length
  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator   =:= '0'                             [ 1 ];
    sequence_number =:= msn_lsb(4)                      [ 4 ];
    header_crc      =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ip_id           =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
    discriminator   =:= '100'                           [ 3 ];
    sequence_number =:= msn_lsb(6)                      [ 6 ];
    header_crc      =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    ip_id           =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1-ID replacement (PT-1 only used for sequential)
  COMPRESSED pt_1_seq_id {
Top   ToC   RFC5225 - Page 89
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator   =:= '101'                               [ 3 ];
    header_crc      =:= crc3(THIS.UVALUE, THIS.ULENGTH)     [ 3 ];
    sequence_number =:= msn_lsb(6)                          [ 6 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator   =:= '110'                               [ 3 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 6) [ 6 ];
    header_crc      =:= crc7(THIS.UVALUE, THIS.ULENGTH)     [ 7 ];
    sequence_number =:= msn_lsb(8)                          [ 8 ];
  }
}

////////////////////////////////////////////
// IP-only profile
////////////////////////////////////////////

iponly_baseheader(profile_value, outer_ip_flag, ip_id_behavior_value,
                  reorder_ratio_value)
{
  UNCOMPRESSED v4 {
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
    tos_tc                                             [  8 ];
    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 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
  }
Top   ToC   RFC5225 - Page 90
  UNCOMPRESSED v6 {
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    outer_headers     =:= baseheader_outer_headers     [ VARIABLE ];
    ip_version        =:= uncompressed_value(4, 6)     [   4 ];
    tos_tc                                             [   8 ];
    flow_label                                         [  20 ];
    payload_length    =:= inferred_ip_v6_length        [  16 ];
    next_header                                        [   8 ];
    ttl_hopl                                           [   8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_IP_0104);
    ENFORCE(profile == profile_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
  }

  DEFAULT {
    ENFORCE(outer_ip_flag == 0);
    tos_tc         =:= static;
    dest_addr      =:= static;
    ttl_hopl       =:= static;
    src_addr       =:= static;
    df             =:= static;
    flow_label     =:= static;
    next_header    =:= static;
    reorder_ratio  =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags_indicator      =:= irregular(1)                  [ 1 ];
    ttl_hopl_indicator   =:= irregular(1)                  [ 1 ];
    tos_tc_indicator     =:= irregular(1)                  [ 1 ];
    reorder_ratio        =:= irregular(2)                  [ 2 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];
    outer_ip_indicator : df : ip_id_behavior_innermost =:=
Top   ToC   RFC5225 - Page 91
      profile_2_3_4_flags_enc(
      flags_indicator.CVALUE, ip_version.UVALUE)           [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
    ttl_hopl =:= static_or_irreg(ttl_hopl_indicator.CVALUE,
      ttl_hopl.ULENGTH)                                    [ 0, 8 ];
    msn                  =:= msn_lsb(8)                    [ 8 ];
    ip_id =:= ip_id_sequential_variable(ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE)                          [ 0, 8, 16 ];
  }

  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator =:= '0'                             [ 1 ];
    msn           =:= msn_lsb(4)                      [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
    discriminator =:= '100'                           [ 3 ];
    msn           =:= msn_lsb(6)                      [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1-ID replacement (PT-1 only used for sequential)
  COMPRESSED pt_1_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '101'                                 [ 3 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)       [ 3 ];
    msn           =:= msn_lsb(6)                            [ 6 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '110'                                 [ 3 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 6) [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    msn           =:= msn_lsb(8)                            [ 8 ];
Top   ToC   RFC5225 - Page 92
  }
}

////////////////////////////////////////////
// UDP-lite/RTP profile
////////////////////////////////////////////

udplite_rtp_baseheader(profile_value, ts_stride_value,
                       time_stride_value, outer_ip_flag,
                       ip_id_behavior_value, reorder_ratio_value,
                       coverage_behavior_value)
{
  UNCOMPRESSED v4 {
    ENFORCE(msn.UVALUE == sequence_number.UVALUE);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
    tos_tc                                             [  8 ];
    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 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dst_port                                           [ 16 ];
    checksum_coverage                                  [ 16 ];
    udp_checksum                                       [ 16 ];
    rtp_version    =:= uncompressed_value(2, 2)        [  2 ];
    pad_bit                                            [  1 ];
    extension                                          [  1 ];
    cc                                                 [  4 ];
    marker                                             [  1 ];
    payload_type                                       [  7 ];
    sequence_number                                    [ 16 ];
    timestamp                                          [ 32 ];
    ssrc                                               [ 32 ];
    csrc_list                                          [ VARIABLE ];
  }

  UNCOMPRESSED v6 {
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
Top   ToC   RFC5225 - Page 93
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 6)        [   4 ];
    tos_tc                                             [   8 ];
    flow_label                                         [  20 ];
    payload_length =:= inferred_ip_v6_length           [  16 ];
    next_header                                        [   8 ];
    ttl_hopl                                           [   8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [  16 ];
    dst_port                                           [  16 ];
    checksum_coverage                                  [  16 ];
    udp_checksum                                       [  16 ];
    rtp_version =:= uncompressed_value(2, 2)           [   2 ];
    pad_bit                                            [   1 ];
    extension                                          [   1 ];
    cc                                                 [   4 ];
    marker                                             [   1 ];
    payload_type                                       [   7 ];
    sequence_number                                    [  16 ];
    timestamp                                          [  32 ];
    ssrc                                               [  32 ];
    csrc_list                                          [ VARIABLE ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_RTP_0107);
    ENFORCE(profile == profile_value);
    ENFORCE(time_stride.UVALUE == time_stride_value);
    ENFORCE(ts_stride.UVALUE == ts_stride_value);
    ENFORCE(coverage_behavior.UVALUE == coverage_behavior_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
    dummy_field =:= field_scaling(ts_stride.UVALUE,
      ts_scaled.UVALUE, timestamp.UVALUE, ts_offset.UVALUE) [ 0 ];
  }

  INITIAL {
    ts_stride     =:= uncompressed_value(32, TS_STRIDE_DEFAULT);
    time_stride   =:= uncompressed_value(32, TIME_STRIDE_DEFAULT);
  }

  DEFAULT {
    ENFORCE(outer_ip_flag == 0);
    tos_tc            =:= static;
Top   ToC   RFC5225 - Page 94
    dest_addr         =:= static;
    ttl_hopl          =:= static;
    src_addr          =:= static;
    df                =:= static;
    flow_label        =:= static;
    next_header       =:= static;
    src_port          =:= static;
    dst_port          =:= static;
    pad_bit           =:= static;
    extension         =:= static;
    cc                =:= static;
    // When marker not present in packets, it is assumed 0
    marker            =:= uncompressed_value(1, 0);
    payload_type      =:= static;
    sequence_number   =:= static;
    timestamp         =:= static;
    ssrc              =:= static;
    csrc_list         =:= static;
    ts_stride         =:= static;
    time_stride       =:= static;
    ts_scaled         =:= static;
    ts_offset         =:= static;
    reorder_ratio     =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    marker               =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags1_indicator     =:= irregular(1)                  [ 1 ];
    flags2_indicator     =:= irregular(1)                  [ 1 ];
    tsc_indicator        =:= irregular(1)                  [ 1 ];
    tss_indicator        =:= irregular(1)                  [ 1 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];

    outer_ip_indicator : ttl_hopl_indicator :
      tos_tc_indicator : df : ip_id_behavior_innermost : reorder_ratio
      =:= profile_1_7_flags1_enc(flags1_indicator.CVALUE,
        ip_version.UVALUE)                                 [ 0, 8 ];
    list_indicator : pt_indicator : tis_indicator : pad_bit :
      extension : coverage_behavior =:=
      profile_7_flags2_enc(flags2_indicator.CVALUE)        [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
    ttl_hopl =:=
Top   ToC   RFC5225 - Page 95
      static_or_irreg(ttl_hopl_indicator.CVALUE, 8)        [ 0, 8 ];
    payload_type =:= pt_irr_or_static(pt_indicator.CVALUE) [ 0, 8 ];
    sequence_number =:=
      sdvl_sn_lsb(sequence_number.ULENGTH)               [ VARIABLE ];
    ip_id =:= ip_id_sequential_variable(ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE)                            [ 0, 8, 16 ];
    ts_scaled =:= variable_scaled_timestamp(tss_indicator.CVALUE,
      tsc_indicator.CVALUE, ts_stride.UVALUE,
      time_stride.UVALUE)                                [ VARIABLE ];
    timestamp =:= variable_unscaled_timestamp(tss_indicator.CVALUE,
      tsc_indicator.CVALUE)                              [ VARIABLE ];
    ts_stride =:= sdvl_or_static(tss_indicator.CVALUE)   [ VARIABLE ];
    time_stride =:= sdvl_or_static(tis_indicator.CVALUE) [ VARIABLE ];
    csrc_list            =:=
        csrc_list_presence(list_indicator.CVALUE,
          cc.UVALUE)                                     [ VARIABLE ];
  }

  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator =:= '0'                             [ 1 ];
    msn           =:= msn_lsb(4)                      [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    timestamp     =:= inferred_scaled_field           [ 0 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
    discriminator =:= '1000'                          [ 4 ];
    msn           =:= msn_lsb(5)                      [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    timestamp     =:= inferred_scaled_field           [ 0 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1 replacement
  COMPRESSED pt_1_rnd {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
    discriminator =:= '101'                                [ 3 ];
    marker        =:= irregular(1)                         [ 1 ];
    msn           =:= msn_lsb(4)                           [ 4 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)      [ 3 ];
  }
Top   ToC   RFC5225 - Page 96
  // UO-1-ID replacement
  COMPRESSED pt_1_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '1001'                                [ 4 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
    msn           =:= msn_lsb(5)                            [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)       [ 3 ];
    timestamp     =:= inferred_scaled_field                 [ 0 ];
  }

  // UO-1-TS replacement
  COMPRESSED pt_1_seq_ts {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '101'                                [ 3 ];
    marker        =:= irregular(1)                         [ 1 ];
    msn           =:= msn_lsb(4)                           [ 4 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)      [ 3 ];
    ip_id         =:= inferred_sequential_ip_id            [ 0 ];
  }

  // UOR-2 replacement
  COMPRESSED pt_2_rnd {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_RANDOM) ||
            (ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_ZERO));
    discriminator =:= '110'                                [ 3 ];
    msn           =:= msn_lsb(7)                           [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 6) [ 6 ];
    marker        =:= irregular(1)                         [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)      [ 7 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '11000'                               [ 5 ];
Top   ToC   RFC5225 - Page 97
    msn           =:= msn_lsb(7)                            [ 7 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 5) [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    timestamp     =:= inferred_scaled_field                 [ 0 ];
  }

  // UOR-2-ID-ext1 replacement (both TS and IP-ID)
  COMPRESSED pt_2_seq_both {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '11001'                               [ 5 ];
    msn           =:= msn_lsb(7)                            [ 7 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 5) [ 5 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 7)  [ 7 ];
    marker        =:= irregular(1)                          [ 1 ];
  }

  // UOR-2-TS replacement
  COMPRESSED pt_2_seq_ts {
    ENFORCE(ts_stride.UVALUE != 0);
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '1101'                               [ 4 ];
    msn           =:= msn_lsb(7)                           [ 7 ];
    ts_scaled     =:= scaled_ts_lsb(time_stride.UVALUE, 5) [ 5 ];
    marker        =:= irregular(1)                         [ 1 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)      [ 7 ];
    ip_id         =:= inferred_sequential_ip_id            [ 0 ];
  }
}

////////////////////////////////////////////
// UDP-lite profile
////////////////////////////////////////////

udplite_baseheader(profile_value, outer_ip_flag, ip_id_behavior_value,
                   reorder_ratio_value, coverage_behavior_value)
{
  UNCOMPRESSED v4 {
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 4)        [  4 ];
    header_length  =:= uncompressed_value(4, 5)        [  4 ];
Top   ToC   RFC5225 - Page 98
    tos_tc                                             [  8 ];
    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 ];
    next_header                                        [  8 ];
    ip_checksum =:= inferred_ip_v4_header_checksum     [ 16 ];
    src_addr                                           [ 32 ];
    dest_addr                                          [ 32 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [ 16 ];
    dst_port                                           [ 16 ];
    checksum_coverage                                  [ 16 ];
    udp_checksum                                       [ 16 ];
  }

  UNCOMPRESSED v6 {
    ENFORCE(ip_id_behavior_innermost.UVALUE == IP_ID_BEHAVIOR_RANDOM);
    outer_headers  =:= baseheader_outer_headers        [ VARIABLE ];
    ip_version     =:= uncompressed_value(4, 6)        [   4 ];
    tos_tc                                             [   8 ];
    flow_label                                         [  20 ];
    payload_length =:= inferred_ip_v6_length           [  16 ];
    next_header                                        [   8 ];
    ttl_hopl                                           [   8 ];
    src_addr                                           [ 128 ];
    dest_addr                                          [ 128 ];
    extension_headers =:= baseheader_extension_headers [ VARIABLE ];
    src_port                                           [  16 ];
    dst_port                                           [  16 ];
    checksum_coverage                                  [  16 ];
    udp_checksum                                       [  16 ];
    df    =:= uncompressed_value(0,0)                  [   0 ];
    ip_id =:= uncompressed_value(0,0)                  [   0 ];
  }

  CONTROL {
    ENFORCE(profile_value == PROFILE_UDPLITE_0108);
    ENFORCE(profile == profile_value);
    ENFORCE(coverage_behavior.UVALUE == coverage_behavior_value);
    ENFORCE(reorder_ratio.UVALUE == reorder_ratio_value);
    ENFORCE(ip_id_behavior_innermost.UVALUE == ip_id_behavior_value);
  }

  DEFAULT {
Top   ToC   RFC5225 - Page 99
    ENFORCE(outer_ip_flag == 0);
    tos_tc            =:= static;
    dest_addr         =:= static;
    ttl_hopl          =:= static;
    src_addr          =:= static;
    df                =:= static;
    flow_label        =:= static;
    next_header       =:= static;
    src_port          =:= static;
    dst_port          =:= static;
    reorder_ratio     =:= static;
    ip_id_behavior_innermost =:= static;
  }

  // Replacement for UOR-2-ext3
  COMPRESSED co_common {
    ENFORCE(outer_ip_flag == outer_ip_indicator.CVALUE);
    discriminator        =:= '11111010'                    [ 8 ];
    ip_id_indicator      =:= irregular(1)                  [ 1 ];
    header_crc   =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    flags_indicator      =:= irregular(1)                  [ 1 ];
    ttl_hopl_indicator   =:= irregular(1)                  [ 1 ];
    tos_tc_indicator     =:= irregular(1)                  [ 1 ];
    reorder_ratio        =:= irregular(2)                  [ 2 ];
    control_crc3         =:= control_crc3_encoding         [ 3 ];
    outer_ip_indicator : df : ip_id_behavior_innermost :
      coverage_behavior  =:=
      profile_8_flags_enc(flags_indicator.CVALUE,
      ip_version.UVALUE)                                   [ 0, 8 ];
    tos_tc =:= static_or_irreg(tos_tc_indicator.CVALUE, 8) [ 0, 8 ];
    ttl_hopl =:= static_or_irreg(ttl_hopl_indicator.CVALUE,
      ttl_hopl.ULENGTH)                                    [ 0, 8 ];
    msn                  =:= msn_lsb(8)                    [ 8 ];
    ip_id =:= ip_id_sequential_variable(ip_id_behavior_innermost.UVALUE,
      ip_id_indicator.CVALUE)                          [ 0, 8, 16 ];
  }

  // UO-0
  COMPRESSED pt_0_crc3 {
    discriminator =:= '0'                             [ 1 ];
    msn           =:= msn_lsb(4)                      [ 4 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH) [ 3 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // New format, Type 0 with strong CRC and more SN bits
  COMPRESSED pt_0_crc7 {
    discriminator =:= '100'                           [ 3 ];
Top   ToC   RFC5225 - Page 100
    msn           =:= msn_lsb(6)                      [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH) [ 7 ];
    ip_id         =:= inferred_sequential_ip_id       [ 0 ];
  }

  // UO-1-ID replacement (PT-1 only used for sequential)
  COMPRESSED pt_1_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '101'                                 [ 3 ];
    header_crc    =:= crc3(THIS.UVALUE, THIS.ULENGTH)       [ 3 ];
    msn           =:= msn_lsb(6)                            [ 6 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 4) [ 4 ];
  }

  // UOR-2-ID replacement
  COMPRESSED pt_2_seq_id {
    ENFORCE((ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL) ||
            (ip_id_behavior_innermost.UVALUE ==
             IP_ID_BEHAVIOR_SEQUENTIAL_SWAPPED));
    discriminator =:= '110'                                 [ 3 ];
    ip_id =:= ip_id_lsb(ip_id_behavior_innermost.UVALUE, 6) [ 6 ];
    header_crc    =:= crc7(THIS.UVALUE, THIS.ULENGTH)       [ 7 ];
    msn           =:= msn_lsb(8)                            [ 8 ];
  }
}



(page 100 continued on part 4)

Next Section