pub broadcast proof fn axiom_slice_addr_no_overflow(s: &[u8])Expand description
ensures
#[trigger] (as_ptr_spec(s) as usize) + s.len() <= usize::MAX,AXIOM: A slice’s one-past-the-end byte address fits in usize.
Rust guarantees that any valid slice’s memory range lies within the
addressable address space, so as_ptr(s) as usize + s.len() * size_of::<T>()
never overflows. We package this as a usize-level fact for T = u8 (the
common case for byte-slice plumbing); other element types can use it after
multiplying by size_of::<T>().