Claim #3 — Cloning a buffer creates a fresh buffer without panics

The sole local trusted operation is assume_init_slice, which casts a borrowed slice of MaybeUninit<u8> to a borrowed slice of u8. Its caller proves that every selected slot is initialized; its assumed contract preserves the slice length and each byte, without assuming decimal correctness or ASCII. Source reasoning supports this narrow boundary: MaybeUninit<u8> has u8's size and alignment, the cast retains the slice metadata, every u8 bit pattern is valid, and the returned shared borrow is tied to the input borrow. The conversion allocates nothing and selects only the suffix proved initialized. This reasoning is not a formal proof of the raw view or physical memory-permission transfer, which remain trusted and are necessary for the returned string guarantee.

The proof also relies on external contracts for core operations, including MaybeUninit writes, unchecked slice selection, array indexing and slice-to-array borrowing, signed unsigned_abs, and from_utf8_unchecked. Callers prove the relevant initialization, bounds, exact lengths and UTF-8 conditions. The array contracts describe the same elements and preserve changes through the borrowed view; unsigned_abs gives the mathematical magnitude even at signed MIN, consistent with core's wrapping absolute-value implementation. The string conversion is assumed to retain bytes when its proved UTF-8 precondition holds. These contracts describe narrow standard operations, but their runtime core bodies are not proved by this crate verification.