164     /// shallow padding, unsafe code may assume that the result of this method
181     /// Unsafe code may assume that the contract of this function is satisfied.
205     /// Unsafe code may assume that `DstLayout` is the correct layout for `T`.
229     /// Unsafe code may assume that `DstLayout` is the correct layout for `T`.
241     /// Unsafe code may assume that `DstLayout` is the correct layout for `[T]`.
571     /// The caller may assume that this implementation is correct, and may rely
573     /// caller may assume that, if `validate_cast_and_convert_metadata` returns
826                 // Assume that `Src` and `Dst` are slice DSTs, and define:  in project()
1963             kani::assume(align.is_power_of_two());  in any()
1964             kani::assume(align < DstLayout::THEORETICAL_MAX_ALIGN);  in any()
1970             kani::assume(  in any()
1994                     kani::assume(size <= DstLayout::MAX_SIZE);  in any()
2008             kani::assume(elem_size < DstLayout::MAX_SIZE);  in any()
2009             kani::assume(offset < DstLayout::MAX_SIZE);  in any()
2020             kani::assume(false);  in prove_requires_dynamic_padding()
2028             kani::assume(false);  in prove_requires_dynamic_padding()
2034             kani::assume(false);  in prove_requires_dynamic_padding()
2040             kani::assume(false);  in prove_requires_dynamic_padding()
2060             kani::assume(max_align.is_power_of_two());  in prove_dst_layout_extend()
2061             kani::assume(base.align <= max_align);  in prove_dst_layout_extend()
2065         kani::assume(matches!(base.size_info, SizeInfo::Sized { .. }));  in prove_dst_layout_extend()
2183             kani::assume(max_align.is_power_of_two());  in prove_dst_layout_extend_dst_panics()
2184             kani::assume(base.align <= max_align);  in prove_dst_layout_extend_dst_panics()
2187         kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..)));  in prove_dst_layout_extend_dst_panics()