pub open spec fn is_valid_ia5_string_spec(bytes: Seq<u8>) -> bool
{ forall |i: int| 0 <= i < bytes.len() ==> #[trigger] bytes[i] <= 127 }