pub open spec fn at_ber_end(input: Seq<u8>) -> bool
{ input.len() == 0 || EOC.spec_parse(input) is Some }