pub open spec fn invert_bytes(bytes: Seq<u8>) -> Seq<u8>
{ bytes.map_values(|b: u8| invert_byte(b)) }