RFC 5225
RObust Header Compression Version 2 (ROHCv2): Profiles for RTP, UDP, IP, ESP and UDP-Lite
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].
// 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 {
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 {
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);
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 ];
}
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)
{
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 {
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 ];
}
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)
{
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 ];
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 {
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 {
}
}
/////////////////////////////////////////////
// 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 {
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 ];
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 ];
}
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 ];
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 ];
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
/////////////////////////////////////////////
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 ];
}
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 {
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 ];
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 {
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 ];
}
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 ];
}
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);
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 {
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 {
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 ];
}
}
// 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 ];
}
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));
}
}
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);
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 ];
}
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 ];
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 {
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);
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 ];
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 ];
}
// 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 ];
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 ];
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);
}
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 {
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 ];
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;
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 {
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 ];
}
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 =:=
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 ];
}
}
////////////////////////////////////////////
// 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);
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;
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 =:=
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 ];
}
// 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 ];
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 ];
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 {
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 ];
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)
