Skip to main content

ber_bit_string_segments_wf

vest_lib::asn1::ber::bit_string

Function ber_bit_string_segments_wf 

Source 
pub open spec fn ber_bit_string_segments_wf(segments: Seq<BitStringSpec>) -> bool
Expand description
{ forall |i: int| 0 <= i < segments.len() - 1 ==> #[trigger] segments[i].unused == 0 }

Constructed BIT STRING segments are concatenable only when every segment except the last has zero unused bits (X.690 ยง8.6.4.2).