pub broadcast proof fn is_ascii_spec_bytes(s: &str)Expand description
ensures
#[trigger] is_ascii(s)
==> (#[trigger] s.spec_bytes() =~= Seq::new(s@.len(), |i| s@.index(i) as u8)),