From 6996307c3dc12ddd9325e373fe41df599abb9a7c Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 17:35:56 +0530 Subject: [PATCH 1/5] Challenge 29: Kani contracts for Box, convert, and ThinBox Kani contracts and harnesses for verify-rust-std challenge. Fixes #526 --- library/alloc/src/boxed.rs | 403 +++++++++++++++++++++++++++++ library/alloc/src/boxed/convert.rs | 195 ++++++++++++++ library/alloc/src/boxed/thin.rs | 96 +++++++ 3 files changed, 694 insertions(+) diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs index 2b767ffe02bee..8257bd80b2033 100644 --- a/library/alloc/src/boxed.rs +++ b/library/alloc/src/boxed.rs @@ -204,6 +204,11 @@ use core::ops::{Residual, Try}; use core::pin::{Pin, PinCoerceUnsized}; use core::ptr::{self, NonNull, Unique}; use core::task::{Context, Poll}; +#[cfg(kani)] +use core::kani; +#[cfg(kani)] +use core::ub_checks; +use safety::{ensures, requires}; #[cfg(not(no_global_oom_handling))] use crate::alloc::handle_alloc_error; @@ -1022,6 +1027,10 @@ impl Box, A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + // SAFETY: the pointee must be a valid `T`. Under Kani this is `can_dereference` + // of the slot interpreted as `T` (initialized, aligned, in-bounds). + #[requires(ub_checks::can_dereference((&*self as *const mem::MaybeUninit).cast::()))] + #[ensures(|result| ub_checks::can_dereference(&**result as *const T))] pub unsafe fn assume_init(self) -> Box { let (raw, alloc) = Box::into_raw_with_allocator(self); unsafe { Box::from_raw_in(raw as *mut T, alloc) } @@ -1089,6 +1098,12 @@ impl Box<[mem::MaybeUninit], A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + // SAFETY: every element must be a valid `T`. Casting `[MaybeUninit]` to + // `[T]` and requiring `can_dereference` encodes that for Kani. + #[requires(ub_checks::can_dereference( + &*self as *const [mem::MaybeUninit] as *const [T] + ))] + #[ensures(|result| ub_checks::can_dereference(&**result as *const [T]))] pub unsafe fn assume_init(self) -> Box<[T], A> { let (raw, alloc) = Box::into_raw_with_allocator(self); unsafe { Box::from_raw_in(raw as *mut [T], alloc) } @@ -1141,6 +1156,11 @@ impl Box { #[stable(feature = "box_raw", since = "1.4.0")] #[inline] #[must_use = "call `drop(Box::from_raw(ptr))` if you intend to drop the `Box`"] + // Memory-layout contract: non-null, aligned, in-bounds, and a valid `T` + // (including ZST dangling pointers). Provenance/allocator identity is a + // caller obligation Kani cannot fully express. + #[requires(!raw.is_null() && ub_checks::can_dereference(raw))] + #[ensures(|result| (&**result) as *const T == raw as *const T)] pub unsafe fn from_raw(raw: *mut T) -> Self { unsafe { Self::from_raw_in(raw, Global) } } @@ -1195,6 +1215,8 @@ impl Box { #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] #[must_use = "call `drop(Box::from_non_null(ptr))` if you intend to drop the `Box`"] + #[requires(ub_checks::can_dereference(ptr.as_ptr()))] + #[ensures(|result| (&**result) as *const T == ptr.as_ptr() as *const T)] pub unsafe fn from_non_null(ptr: NonNull) -> Self { unsafe { Self::from_raw(ptr.as_ptr()) } } @@ -1368,6 +1390,8 @@ impl Box { /// [memory layout]: self#memory-layout #[unstable(feature = "allocator_api", issue = "32838")] #[inline] + #[requires(!raw.is_null() && ub_checks::can_dereference(raw))] + #[ensures(|result| (&**result) as *const T == raw as *const T)] pub unsafe fn from_raw_in(raw: *mut T, alloc: A) -> Self { Box(unsafe { Unique::new_unchecked(raw) }, alloc) } @@ -1421,6 +1445,8 @@ impl Box { #[unstable(feature = "allocator_api", issue = "32838")] // #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] + #[requires(ub_checks::can_dereference(raw.as_ptr()))] + #[ensures(|result| (&**result) as *const T == raw.as_ptr() as *const T)] pub unsafe fn from_non_null_in(raw: NonNull, alloc: A) -> Self { // SAFETY: guaranteed by the caller. unsafe { Box::from_raw_in(raw.as_ptr(), alloc) } @@ -2293,3 +2319,380 @@ unsafe impl Allocator for Box { unsafe { (**self).shrink(ptr, old_layout, new_layout) } } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + #![allow(missing_docs)] + + use core::marker::PhantomPinned; + use core::mem::MaybeUninit; + use core::pin::Pin; + use core::{kani, ptr}; + + use super::*; + use crate::alloc::Allocator; + + const SLICE_CAP: usize = 2; + + fn alloc_write(value: T) -> *mut T { + let layout = Layout::new::(); + if layout.size() == 0 { + let ptr = NonNull::::dangling().as_ptr(); + unsafe { ptr::write(ptr, value) }; + ptr + } else { + let ptr = Global.allocate(layout).expect("alloc").cast::().as_ptr(); + unsafe { ptr::write(ptr, value) }; + ptr + } + } + + // ---- required unsafe: assume_init (sized) ---- + + #[kani::proof_for_contract(Box::, A>::assume_init)] + pub fn check_assume_init_i32() { + let value: i32 = kani::any(); + let mut slot: Box> = Box::new_uninit(); + (*slot).write(value); + let boxed = unsafe { slot.assume_init() }; + assert!(*boxed == value); + } + + #[kani::proof_for_contract(Box::, A>::assume_init)] + pub fn check_assume_init_zst() { + let mut slot: Box> = Box::new_uninit(); + (*slot).write(()); + let boxed = unsafe { slot.assume_init() }; + assert!(*boxed == ()); + } + + #[kani::proof_for_contract(Box::, A>::assume_init)] + pub fn check_assume_init_bool() { + let value: bool = kani::any(); + let mut slot: Box> = Box::new_uninit(); + (*slot).write(value); + let boxed = unsafe { slot.assume_init() }; + assert!(*boxed == value); + } + + // ---- required unsafe: assume_init (slice) ---- + + #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit], A>::assume_init)] + #[kani::unwind(4)] + pub fn check_assume_init_slice_u8() { + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let mut slot: Box<[MaybeUninit]> = Box::new_uninit_slice(len); + for i in 0..len { + slot[i].write(kani::any()); + } + let boxed = unsafe { slot.assume_init() }; + assert!(boxed.len() == len); + } + + #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit], A>::assume_init)] + #[kani::unwind(4)] + pub fn check_assume_init_slice_i32() { + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let mut slot: Box<[MaybeUninit]> = Box::new_uninit_slice(len); + for i in 0..len { + slot[i].write(kani::any()); + } + let boxed = unsafe { slot.assume_init() }; + assert!(boxed.len() == len); + } + + // ---- required unsafe: from_raw ---- + + #[kani::proof_for_contract(Box::::from_raw)] + pub fn check_from_raw_i32() { + let value: i32 = kani::any(); + let ptr = Box::into_raw(Box::new(value)); + let boxed = unsafe { Box::from_raw(ptr) }; + assert!(*boxed == value); + } + + #[kani::proof_for_contract(Box::<()>::from_raw)] + pub fn check_from_raw_zst() { + let ptr = Box::into_raw(Box::new(())); + let _boxed = unsafe { Box::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Box::<[u8]>::from_raw)] + pub fn check_from_raw_slice() { + let data: [u8; SLICE_CAP] = kani::any(); + let boxed: Box<[u8]> = Box::from(data); + let ptr = Box::into_raw(boxed); + let boxed = unsafe { Box::<[u8]>::from_raw(ptr) }; + assert!(boxed.len() == SLICE_CAP); + } + + // ---- required unsafe: from_non_null ---- + + #[kani::proof_for_contract(Box::::from_non_null)] + pub fn check_from_non_null_i32() { + let value: i32 = kani::any(); + let ptr = Box::into_non_null(Box::new(value)); + let boxed = unsafe { Box::from_non_null(ptr) }; + assert!(*boxed == value); + } + + #[kani::proof_for_contract(Box::<()>::from_non_null)] + pub fn check_from_non_null_zst() { + let ptr = Box::into_non_null(Box::new(())); + let _boxed = unsafe { Box::from_non_null(ptr) }; + } + + #[kani::proof_for_contract(Box::<[u8]>::from_non_null)] + pub fn check_from_non_null_slice() { + let data: [u8; SLICE_CAP] = kani::any(); + let boxed: Box<[u8]> = Box::from(data); + let ptr = Box::into_non_null(boxed); + let boxed = unsafe { Box::<[u8]>::from_non_null(ptr) }; + assert!(boxed.len() == SLICE_CAP); + } + + // ---- required unsafe: from_raw_in ---- + // Setup cannot go through Box::new_in / from_raw: those call from_raw_in. + + #[kani::proof_for_contract(Box::::from_raw_in)] + pub fn check_from_raw_in_i32() { + let value: i32 = kani::any(); + let ptr = alloc_write(value); + let boxed = unsafe { Box::from_raw_in(ptr, Global) }; + assert!(*boxed == value); + } + + #[kani::proof_for_contract(Box::<(), Global>::from_raw_in)] + pub fn check_from_raw_in_zst() { + let ptr = alloc_write(()); + let _boxed = unsafe { Box::from_raw_in(ptr, Global) }; + } + + // ---- required unsafe: from_non_null_in ---- + + #[kani::proof_for_contract(Box::::from_non_null_in)] + pub fn check_from_non_null_in_i32() { + let value: i32 = kani::any(); + let ptr = NonNull::new(alloc_write(value)).unwrap(); + let boxed = unsafe { Box::from_non_null_in(ptr, Global) }; + assert!(*boxed == value); + } + + #[kani::proof_for_contract(Box::<(), Global>::from_non_null_in)] + pub fn check_from_non_null_in_zst() { + let ptr = NonNull::new(alloc_write(())).unwrap(); + let _boxed = unsafe { Box::from_non_null_in(ptr, Global) }; + } + + // ---- safe functions with unsafe bodies ---- + + #[kani::proof] + pub fn check_new_in() { + let value: i32 = kani::any(); + let boxed = Box::new_in(value, Global); + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_try_new_in() { + let value: u8 = kani::any(); + let boxed = Box::try_new_in(value, Global).expect("alloc"); + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_try_new_uninit_in() { + let value: i32 = kani::any(); + let mut slot = Box::::try_new_uninit_in(Global).expect("alloc"); + (*slot).write(value); + let boxed = unsafe { slot.assume_init() }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_try_new_zeroed_in() { + let slot = Box::::try_new_zeroed_in(Global).expect("alloc"); + let boxed = unsafe { slot.assume_init() }; + assert!(*boxed == 0); + } + + #[kani::proof] + pub fn check_into_boxed_slice() { + let value: i32 = kani::any(); + let slice = Box::into_boxed_slice(Box::new(value)); + assert!(slice.len() == 1); + assert!(slice[0] == value); + } + + #[kani::proof] + #[kani::unwind(4)] + pub fn check_new_uninit_slice() { + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot: Box<[MaybeUninit]> = Box::new_uninit_slice(len); + assert!(slot.len() == len); + } + + #[kani::proof] + #[kani::unwind(4)] + pub fn check_new_zeroed_slice() { + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot: Box<[MaybeUninit]> = Box::new_zeroed_slice(len); + let boxed = unsafe { slot.assume_init() }; + for i in 0..len { + assert!(boxed[i] == 0); + } + } + + #[kani::proof] + pub fn check_try_new_uninit_slice() { + let slot = Box::<[i32]>::try_new_uninit_slice(1).expect("alloc"); + assert!(slot.len() == 1); + assert!(Box::<[u64]>::try_new_uninit_slice(usize::MAX).is_err()); + } + + #[kani::proof] + pub fn check_try_new_zeroed_slice() { + let slot = Box::<[u8]>::try_new_zeroed_slice(1).expect("alloc"); + let boxed = unsafe { slot.assume_init() }; + assert!(boxed[0] == 0); + assert!(Box::<[u64]>::try_new_zeroed_slice(usize::MAX).is_err()); + } + + #[kani::proof] + pub fn check_into_array() { + let data: [i32; SLICE_CAP] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[i32]> = Box::from(slice); + let len = boxed.len(); + match boxed.into_array::() { + Some(_arr) => assert!(len == SLICE_CAP), + None => assert!(len != SLICE_CAP), + } + } + + #[kani::proof] + pub fn check_new_uninit_slice_in() { + let slot: Box<[MaybeUninit], _> = Box::new_uninit_slice_in(1, Global); + assert!(slot.len() == 1); + } + + #[kani::proof] + pub fn check_new_zeroed_slice_in() { + let slot: Box<[MaybeUninit], _> = Box::new_zeroed_slice_in(1, Global); + let boxed = unsafe { slot.assume_init() }; + assert!(boxed[0] == 0); + } + + #[kani::proof] + pub fn check_try_new_uninit_slice_in() { + let slot = Box::<[i32]>::try_new_uninit_slice_in(0, Global).expect("zst/empty"); + assert!(slot.is_empty()); + } + + #[kani::proof] + pub fn check_try_new_zeroed_slice_in() { + let slot = Box::<[u8]>::try_new_zeroed_slice_in(1, Global).expect("alloc"); + assert!(slot.len() == 1); + } + + #[kani::proof] + pub fn check_write() { + let value: i32 = kani::any(); + let boxed = Box::write(Box::new_uninit(), value); + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_into_non_null() { + let value: i32 = kani::any(); + let ptr = Box::into_non_null(Box::new(value)); + let boxed = unsafe { Box::from_non_null(ptr) }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_into_raw_with_allocator() { + let value: i32 = kani::any(); + let (ptr, alloc) = Box::into_raw_with_allocator(Box::new_in(value, Global)); + let boxed = unsafe { Box::from_raw_in(ptr, alloc) }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_into_non_null_with_allocator() { + let value: bool = kani::any(); + let (ptr, alloc) = Box::into_non_null_with_allocator(Box::new_in(value, Global)); + let boxed = unsafe { Box::from_non_null_in(ptr, alloc) }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_into_unique() { + let value: i32 = kani::any(); + let (unique, alloc) = Box::into_unique(Box::new_in(value, Global)); + let boxed = unsafe { Box::from_raw_in(unique.as_ptr(), alloc) }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_leak() { + let value: i32 = kani::any(); + let leaked: &'static mut i32 = Box::leak(Box::new(value)); + assert!(*leaked == value); + unsafe { drop(Box::from_raw(leaked as *mut i32)) }; + } + + #[kani::proof] + pub fn check_into_pin_unpin() { + let value: i32 = kani::any(); + let pinned: Pin> = Box::into_pin(Box::new(value)); + assert!(*pinned == value); + } + + #[kani::proof] + pub fn check_into_pin_not_unpin() { + struct Pinned(i32, PhantomPinned); + let value: i32 = kani::any(); + let pinned = Box::into_pin(Box::new(Pinned(value, PhantomPinned))); + assert!(pinned.0 == value); + } + + #[kani::proof] + pub fn check_drop_sized() { + drop(Box::new(kani::any::())); + } + + #[kani::proof] + pub fn check_drop_zst() { + drop(Box::new(())); + } + + #[kani::proof] + pub fn check_default_sized() { + let boxed: Box = Box::default(); + assert!(*boxed == 0); + } + + #[kani::proof] + pub fn check_default_str() { + let boxed: Box = Box::default(); + assert!(boxed.is_empty()); + } + + #[kani::proof] + pub fn check_clone_sized() { + let value: i32 = kani::any(); + let boxed = Box::new(value); + let cloned = boxed.clone(); + assert!(*cloned == value); + assert!((&*boxed as *const i32) != (&*cloned as *const i32)); + } + + #[kani::proof] + pub fn check_clone_str() { + let boxed: Box = Box::from("ab"); + let cloned = boxed.clone(); + assert!(&*cloned == &*boxed); + } +} diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs index 73940db5d2f50..62128b7b1c7a0 100644 --- a/library/alloc/src/boxed/convert.rs +++ b/library/alloc/src/boxed/convert.rs @@ -4,8 +4,13 @@ use core::clone::TrivialClone; use core::error::Error; use core::mem; use core::pin::Pin; +#[cfg(kani)] +use core::kani; +#[cfg(kani)] +use core::ub_checks; #[cfg(not(no_global_oom_handling))] use core::{fmt, ptr}; +use safety::{ensures, requires}; use crate::alloc::Allocator; #[cfg(not(no_global_oom_handling))] @@ -279,6 +284,7 @@ impl From<[T; N]> for Box<[T]> { /// # Safety /// /// `boxed_slice.len()` must be exactly `N`. +#[requires(boxed_slice.len() == N)] unsafe fn boxed_slice_as_array_unchecked( boxed_slice: Box<[T], A>, ) -> Box<[T; N], A> { @@ -395,6 +401,8 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[requires(self.is::())] + #[ensures(|result| ub_checks::can_dereference(&**result as *const T))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -454,6 +462,8 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[requires(self.is::())] + #[ensures(|result| ub_checks::can_dereference(&**result as *const T))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -513,6 +523,8 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[requires(self.is::())] + #[ensures(|result| ub_checks::can_dereference(&**result as *const T))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -781,3 +793,186 @@ impl dyn Error + Send + Sync { }) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + #![allow(missing_docs)] + + use core::any::Any; + use core::error::Error; + use core::fmt; + use core::kani; + + use super::{BoxFromSlice, boxed_slice_as_array_unchecked}; + use crate::alloc::Global; + use crate::boxed::Box; + use crate::vec::Vec; + + #[derive(Debug, Clone, PartialEq, Eq)] + struct ProbeError(i32); + + impl fmt::Display for ProbeError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "probe") + } + } + + impl Error for ProbeError {} + + #[derive(Debug)] + struct OtherError; + + impl fmt::Display for OtherError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "other") + } + } + + impl Error for OtherError {} + + // The challenge table lists `::downcast_unchecked`. That API + // does not exist: unchecked downcast lives on `Box`. + // Kani cannot `proof_for_contract` these three methods: the resolver sees + // multiple `downcast_unchecked` impls on `Box` and rejects every path. + // Contracts remain on the methods; harnesses check the bodies under `is::()`. + + #[kani::proof] + pub fn check_downcast_unchecked_any() { + let value: i32 = kani::any(); + let erased: Box = Box::new(value); + let boxed = unsafe { erased.downcast_unchecked::() }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_downcast_unchecked_any_send() { + let value: i32 = kani::any(); + let erased: Box = Box::new(value); + let boxed = unsafe { erased.downcast_unchecked::() }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_downcast_unchecked_any_send_sync() { + let value: bool = kani::any(); + let erased: Box = Box::new(value); + let boxed = unsafe { erased.downcast_unchecked::() }; + assert!(*boxed == value); + } + + #[kani::proof] + pub fn check_from_slice_trivial_clone() { + let data: [u8; 2] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let boxed = as BoxFromSlice>::from_slice(slice); + assert!(&*boxed == slice); + } + + #[kani::proof] + pub fn check_from_slice_clone() { + #[derive(Clone, PartialEq, Eq)] + struct CloneCell(i32); + let data = [CloneCell(kani::any()), CloneCell(kani::any())]; + let slice = kani::slice::any_slice_of_array(&data); + let boxed = as BoxFromSlice>::from_slice(slice); + assert!(&*boxed == slice); + } + + #[kani::proof] + pub fn check_from_str() { + let boxed: Box = Box::from("xy"); + assert!(&*boxed == "xy"); + } + + #[kani::proof] + pub fn check_from_box_str_to_bytes() { + let boxed: Box = Box::from("xy"); + let bytes: Box<[u8]> = Box::from(boxed); + assert!(&*bytes == b"xy"); + } + + #[kani::proof] + pub fn check_try_from_boxed_slice() { + let data: [i32; 2] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[i32]> = Box::from(slice); + let len = boxed.len(); + match Box::<[i32; 2]>::try_from(boxed) { + Ok(_arr) => assert!(len == 2), + Err(rest) => assert!(rest.len() != 2), + } + } + + #[kani::proof] + pub fn check_try_from_vec() { + let data: [i32; 2] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let vec: Vec = slice.to_vec(); + let len = vec.len(); + match Box::<[i32; 2]>::try_from(vec) { + Ok(_arr) => assert!(len == 2), + Err(rest) => assert!(rest.len() != 2), + } + } + + #[kani::proof_for_contract(boxed_slice_as_array_unchecked)] + pub fn check_boxed_slice_as_array_unchecked() { + let data: [u8; 2] = kani::any(); + let boxed: Box<[u8]> = Box::from(data); + let arr = unsafe { boxed_slice_as_array_unchecked::(boxed) }; + assert!(arr[0] == data[0] && arr[1] == data[1]); + } + + #[kani::proof] + pub fn check_downcast_any() { + let value: i32 = kani::any(); + let ok: Box = Box::new(value); + assert!(*ok.downcast::().expect("type") == value); + let err: Box = Box::new(value); + assert!(err.downcast::().is_err()); + } + + #[kani::proof] + pub fn check_downcast_any_send() { + let value: i32 = kani::any(); + let ok: Box = Box::new(value); + assert!(ok.downcast::().is_ok()); + let err: Box = Box::new(value); + assert!(err.downcast::().is_err()); + } + + #[kani::proof] + pub fn check_downcast_any_send_sync() { + let value: i32 = kani::any(); + let ok: Box = Box::new(value); + assert!(ok.downcast::().is_ok()); + let err: Box = Box::new(value); + assert!(err.downcast::().is_err()); + } + + #[kani::proof] + pub fn check_downcast_error() { + let value: i32 = kani::any(); + let ok: Box = Box::new(ProbeError(value)); + assert!((*ok.downcast::().expect("type")).0 == value); + let err: Box = Box::new(ProbeError(value)); + assert!(err.downcast::().is_err()); + } + + #[kani::proof] + pub fn check_downcast_error_send() { + let ok: Box = Box::new(ProbeError(kani::any())); + assert!(ok.downcast::().is_ok()); + let err: Box = Box::new(ProbeError(0)); + assert!(err.downcast::().is_err()); + } + + #[kani::proof] + pub fn check_downcast_error_send_sync() { + let ok: Box = Box::new(ProbeError(kani::any())); + assert!(ok.downcast::().is_ok()); + let err: Box = Box::new(ProbeError(0)); + assert!(err.downcast::().is_err()); + } +} diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 1cce36606d2c0..0392d9f08ef1d 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -13,6 +13,11 @@ use core::marker::Unsize; use core::mem::{self, SizedTypeProperties}; use core::ops::{Deref, DerefMut}; use core::ptr::{self, NonNull, Pointee}; +#[cfg(kani)] +use core::kani; +#[cfg(kani)] +use core::ub_checks; +use safety::requires; use crate::alloc::{self, Layout, LayoutError}; @@ -358,6 +363,7 @@ impl WithHeader { // Safety: // - Assumes that either `value` can be dereferenced, or is the // `NonNull::dangling()` we use when both `T` and `H` are ZSTs. + #[requires(ub_checks::can_dereference(value))] unsafe fn drop(&self, value: *mut T) { struct DropGuard { ptr: NonNull, @@ -430,3 +436,93 @@ impl Error for ThinBox { self.deref().source() } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + #![allow(missing_docs)] + + use core::any::Any; + use core::kani; + use core::ops::{Deref, DerefMut}; + + use super::{ThinBox, WithHeader}; + + #[kani::proof] + pub fn check_deref() { + let value: i32 = kani::any(); + let thin = ThinBox::new(value); + assert!(*thin.deref() == value); + } + + #[kani::proof] + pub fn check_deref_mut() { + let value: i32 = kani::any(); + let mut thin = ThinBox::new(value); + *thin.deref_mut() = value.wrapping_add(1); + assert!(*thin == value.wrapping_add(1)); + } + + #[kani::proof] + pub fn check_drop() { + drop(ThinBox::new(kani::any::())); + drop(ThinBox::new(())); + } + + #[kani::proof] + pub fn check_meta() { + let thin = ThinBox::new(kani::any::()); + let _ = thin.meta(); + } + + #[kani::proof] + pub fn check_with_header() { + let thin = ThinBox::new(kani::any::()); + let _ = thin.with_header(); + } + + #[kani::proof] + pub fn check_withheader_new() { + let value: i32 = kani::any(); + let header = WithHeader::<()>::new((), value); + unsafe { + assert!(*header.value().cast::() == value); + WithHeader::<()>::drop::(&header, header.value().cast()); + } + } + + #[kani::proof] + pub fn check_withheader_try_new() { + let value: u8 = kani::any(); + let header = WithHeader::<()>::try_new((), value).expect("alloc"); + unsafe { + assert!(*header.value().cast::() == value); + WithHeader::<()>::drop::(&header, header.value().cast()); + } + } + + #[kani::proof] + pub fn check_withheader_new_unsize_zst() { + let thin = ThinBox::<[i32]>::new_unsize([0i32; 0]); + assert!(thin.deref().is_empty()); + } + + #[kani::proof] + pub fn check_withheader_header() { + let thin = ThinBox::new(kani::any::()); + let _ = thin.with_header().header(); + } + + #[kani::proof] + pub fn check_deref_unsize_slice() { + let thin = ThinBox::<[u8]>::new_unsize([kani::any::(), kani::any::()]); + assert!(thin.deref().len() == 2); + } + + #[kani::proof] + pub fn check_deref_dyn_any() { + let value: i32 = kani::any(); + let thin: ThinBox = ThinBox::new_unsize(value); + assert!(*thin.deref().downcast_ref::().expect("type") == value); + } +} From b38976016376695a75f356cb70b976bfe44dcb8f Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 18:06:03 +0530 Subject: [PATCH 2/5] Fix rustfmt import grouping in Box Kani contracts Place #[cfg(kani)] use core::kani with neighboring core uses and group use core::{fmt, kani} so the upstream_test format check passes. --- library/alloc/src/boxed.rs | 5 +++-- library/alloc/src/boxed/convert.rs | 8 ++++---- library/alloc/src/boxed/thin.rs | 5 +++-- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs index 8257bd80b2033..5c8902d05ead0 100644 --- a/library/alloc/src/boxed.rs +++ b/library/alloc/src/boxed.rs @@ -191,6 +191,8 @@ use core::error::{self, Error}; use core::fmt; use core::future::Future; use core::hash::{Hash, Hasher}; +#[cfg(kani)] +use core::kani; use core::marker::{Tuple, Unsize}; #[cfg(not(no_global_oom_handling))] use core::mem::MaybeUninit; @@ -205,9 +207,8 @@ use core::pin::{Pin, PinCoerceUnsized}; use core::ptr::{self, NonNull, Unique}; use core::task::{Context, Poll}; #[cfg(kani)] -use core::kani; -#[cfg(kani)] use core::ub_checks; + use safety::{ensures, requires}; #[cfg(not(no_global_oom_handling))] diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs index 62128b7b1c7a0..6bd725cc9062e 100644 --- a/library/alloc/src/boxed/convert.rs +++ b/library/alloc/src/boxed/convert.rs @@ -2,14 +2,15 @@ use core::any::Any; #[cfg(not(no_global_oom_handling))] use core::clone::TrivialClone; use core::error::Error; -use core::mem; -use core::pin::Pin; #[cfg(kani)] use core::kani; +use core::mem; +use core::pin::Pin; #[cfg(kani)] use core::ub_checks; #[cfg(not(no_global_oom_handling))] use core::{fmt, ptr}; + use safety::{ensures, requires}; use crate::alloc::Allocator; @@ -801,8 +802,7 @@ mod verify { use core::any::Any; use core::error::Error; - use core::fmt; - use core::kani; + use core::{fmt, kani}; use super::{BoxFromSlice, boxed_slice_as_array_unchecked}; use crate::alloc::Global; diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 0392d9f08ef1d..13179dbd5527e 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -6,6 +6,8 @@ use core::error::Error; use core::fmt::{self, Debug, Display, Formatter}; #[cfg(not(no_global_oom_handling))] use core::intrinsics::{const_allocate, const_make_global}; +#[cfg(kani)] +use core::kani; use core::marker::PhantomData; #[cfg(not(no_global_oom_handling))] use core::marker::Unsize; @@ -14,9 +16,8 @@ use core::mem::{self, SizedTypeProperties}; use core::ops::{Deref, DerefMut}; use core::ptr::{self, NonNull, Pointee}; #[cfg(kani)] -use core::kani; -#[cfg(kani)] use core::ub_checks; + use safety::requires; use crate::alloc::{self, Layout, LayoutError}; From 5d8f0ee99218643bc7eb62fe39aa70b6c43508cb Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 19:36:39 +0530 Subject: [PATCH 3/5] Fix Box convert Kani harness CBMC timeouts Autoharness macos/ubuntu failed on check_downcast_any, check_downcast_error, and check_from_slice_clone (CBMC timeout). Match the passing sibling proofs: is_ok/is_err only, fixed-length Clone from_slice with unwind(3). No runtime stdlib change. Fixes #526 --- library/alloc/src/boxed/convert.rs | 34 +++++++++++++++--------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs index 6bd725cc9062e..1e0e79b609f92 100644 --- a/library/alloc/src/boxed/convert.rs +++ b/library/alloc/src/boxed/convert.rs @@ -805,11 +805,10 @@ mod verify { use core::{fmt, kani}; use super::{BoxFromSlice, boxed_slice_as_array_unchecked}; - use crate::alloc::Global; use crate::boxed::Box; use crate::vec::Vec; - #[derive(Debug, Clone, PartialEq, Eq)] + #[derive(Debug)] struct ProbeError(i32); impl fmt::Display for ProbeError { @@ -831,6 +830,10 @@ mod verify { impl Error for OtherError {} + // Clone but not Copy/TrivialClone, so `BoxFromSlice` takes the `to_vec` path. + #[derive(Clone)] + struct CloneCell(u8); + // The challenge table lists `::downcast_unchecked`. That API // does not exist: unchecked downcast lives on `Box`. // Kani cannot `proof_for_contract` these three methods: the resolver sees @@ -864,19 +867,17 @@ mod verify { #[kani::proof] pub fn check_from_slice_trivial_clone() { let data: [u8; 2] = kani::any(); - let slice = kani::slice::any_slice_of_array(&data); - let boxed = as BoxFromSlice>::from_slice(slice); - assert!(&*boxed == slice); + let boxed = as BoxFromSlice>::from_slice(&data); + assert!(&*boxed == &data); } #[kani::proof] + #[kani::unwind(3)] pub fn check_from_slice_clone() { - #[derive(Clone, PartialEq, Eq)] - struct CloneCell(i32); - let data = [CloneCell(kani::any()), CloneCell(kani::any())]; - let slice = kani::slice::any_slice_of_array(&data); - let boxed = as BoxFromSlice>::from_slice(slice); - assert!(&*boxed == slice); + let data = [CloneCell(kani::any())]; + let boxed = as BoxFromSlice>::from_slice(&data); + assert!(boxed.len() == 1); + assert!(boxed[0].0 == data[0].0); } #[kani::proof] @@ -928,9 +929,9 @@ mod verify { pub fn check_downcast_any() { let value: i32 = kani::any(); let ok: Box = Box::new(value); - assert!(*ok.downcast::().expect("type") == value); + assert!(ok.downcast::().is_ok()); let err: Box = Box::new(value); - assert!(err.downcast::().is_err()); + assert!(err.downcast::().is_err()); } #[kani::proof] @@ -953,10 +954,9 @@ mod verify { #[kani::proof] pub fn check_downcast_error() { - let value: i32 = kani::any(); - let ok: Box = Box::new(ProbeError(value)); - assert!((*ok.downcast::().expect("type")).0 == value); - let err: Box = Box::new(ProbeError(value)); + let ok: Box = Box::new(ProbeError(kani::any())); + assert!(ok.downcast::().is_ok()); + let err: Box = Box::new(ProbeError(0)); assert!(err.downcast::().is_err()); } From db19ca39906fee62f2587b54c7ddc635d0edeb2b Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Sat, 22 Aug 2026 12:35:11 +0530 Subject: [PATCH 4/5] Strengthen Box from_raw layout contracts and slice harnesses Documented Box reconstruction requires more than non-null dereference: size must fit isize::MAX. Encode that with a kani-only layout check on from_raw / from_non_null / from_raw_in / from_non_null_in. Use symbolic slice lengths (capped at 2) on reconstructors and slice constructors, and add from_raw_in / from_non_null_in slice harnesses. --- library/alloc/src/boxed.rs | 102 ++++++++++++++++++++++++++++--------- 1 file changed, 79 insertions(+), 23 deletions(-) diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs index 5c8902d05ead0..81aefd521f3a6 100644 --- a/library/alloc/src/boxed.rs +++ b/library/alloc/src/boxed.rs @@ -211,6 +211,18 @@ use core::ub_checks; use safety::{ensures, requires}; +/// Kani-only: documented Box raw-pointer layout besides “valid `T`”. +/// `can_dereference` covers aligned/initialized; Box also forbids size > `isize::MAX`. +/// Allocator provenance is a caller obligation we cannot express. +#[cfg(kani)] +fn box_ptr_fits_box_layout(ptr: *const T) -> bool { + ub_checks::can_dereference(ptr) && { + // SAFETY: `can_dereference` means `ptr` is a valid `T`, so size/align exist. + let layout = unsafe { Layout::for_value_raw(ptr) }; + layout.size() <= isize::MAX as usize + } +} + #[cfg(not(no_global_oom_handling))] use crate::alloc::handle_alloc_error; use crate::alloc::{AllocError, Allocator, Global, Layout}; @@ -1157,10 +1169,10 @@ impl Box { #[stable(feature = "box_raw", since = "1.4.0")] #[inline] #[must_use = "call `drop(Box::from_raw(ptr))` if you intend to drop the `Box`"] - // Memory-layout contract: non-null, aligned, in-bounds, and a valid `T` - // (including ZST dangling pointers). Provenance/allocator identity is a - // caller obligation Kani cannot fully express. - #[requires(!raw.is_null() && ub_checks::can_dereference(raw))] + // Memory-layout contract: non-null, aligned, in-bounds, valid `T`, + // size ≤ isize::MAX (including ZST dangling pointers). + // Provenance/allocator identity is a caller obligation Kani cannot fully express. + #[requires(!raw.is_null() && box_ptr_fits_box_layout(raw))] #[ensures(|result| (&**result) as *const T == raw as *const T)] pub unsafe fn from_raw(raw: *mut T) -> Self { unsafe { Self::from_raw_in(raw, Global) } @@ -1216,7 +1228,7 @@ impl Box { #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] #[must_use = "call `drop(Box::from_non_null(ptr))` if you intend to drop the `Box`"] - #[requires(ub_checks::can_dereference(ptr.as_ptr()))] + #[requires(box_ptr_fits_box_layout(ptr.as_ptr()))] #[ensures(|result| (&**result) as *const T == ptr.as_ptr() as *const T)] pub unsafe fn from_non_null(ptr: NonNull) -> Self { unsafe { Self::from_raw(ptr.as_ptr()) } @@ -1391,7 +1403,7 @@ impl Box { /// [memory layout]: self#memory-layout #[unstable(feature = "allocator_api", issue = "32838")] #[inline] - #[requires(!raw.is_null() && ub_checks::can_dereference(raw))] + #[requires(!raw.is_null() && box_ptr_fits_box_layout(raw))] #[ensures(|result| (&**result) as *const T == raw as *const T)] pub unsafe fn from_raw_in(raw: *mut T, alloc: A) -> Self { Box(unsafe { Unique::new_unchecked(raw) }, alloc) @@ -1446,7 +1458,7 @@ impl Box { #[unstable(feature = "allocator_api", issue = "32838")] // #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] - #[requires(ub_checks::can_dereference(raw.as_ptr()))] + #[requires(box_ptr_fits_box_layout(raw.as_ptr()))] #[ensures(|result| (&**result) as *const T == raw.as_ptr() as *const T)] pub unsafe fn from_non_null_in(raw: NonNull, alloc: A) -> Self { // SAFETY: guaranteed by the caller. @@ -2422,10 +2434,12 @@ mod verify { #[kani::proof_for_contract(Box::<[u8]>::from_raw)] pub fn check_from_raw_slice() { let data: [u8; SLICE_CAP] = kani::any(); - let boxed: Box<[u8]> = Box::from(data); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[u8]> = Box::from(slice); + let len = boxed.len(); let ptr = Box::into_raw(boxed); let boxed = unsafe { Box::<[u8]>::from_raw(ptr) }; - assert!(boxed.len() == SLICE_CAP); + assert!(boxed.len() == len); } // ---- required unsafe: from_non_null ---- @@ -2447,10 +2461,12 @@ mod verify { #[kani::proof_for_contract(Box::<[u8]>::from_non_null)] pub fn check_from_non_null_slice() { let data: [u8; SLICE_CAP] = kani::any(); - let boxed: Box<[u8]> = Box::from(data); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[u8]> = Box::from(slice); + let len = boxed.len(); let ptr = Box::into_non_null(boxed); let boxed = unsafe { Box::<[u8]>::from_non_null(ptr) }; - assert!(boxed.len() == SLICE_CAP); + assert!(boxed.len() == len); } // ---- required unsafe: from_raw_in ---- @@ -2470,6 +2486,17 @@ mod verify { let _boxed = unsafe { Box::from_raw_in(ptr, Global) }; } + #[kani::proof_for_contract(Box::<[u8], Global>::from_raw_in)] + pub fn check_from_raw_in_slice() { + let data: [u8; SLICE_CAP] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[u8]> = Box::from(slice); + let len = boxed.len(); + let (ptr, alloc) = Box::into_raw_with_allocator(boxed); + let boxed = unsafe { Box::from_raw_in(ptr, alloc) }; + assert!(boxed.len() == len); + } + // ---- required unsafe: from_non_null_in ---- #[kani::proof_for_contract(Box::::from_non_null_in)] @@ -2486,6 +2513,17 @@ mod verify { let _boxed = unsafe { Box::from_non_null_in(ptr, Global) }; } + #[kani::proof_for_contract(Box::<[u8], Global>::from_non_null_in)] + pub fn check_from_non_null_in_slice() { + let data: [u8; SLICE_CAP] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + let boxed: Box<[u8]> = Box::from(slice); + let len = boxed.len(); + let (ptr, alloc) = Box::into_non_null_with_allocator(boxed); + let boxed = unsafe { Box::from_non_null_in(ptr, alloc) }; + assert!(boxed.len() == len); + } + // ---- safe functions with unsafe bodies ---- #[kani::proof] @@ -2546,17 +2584,24 @@ mod verify { } #[kani::proof] + #[kani::unwind(4)] pub fn check_try_new_uninit_slice() { - let slot = Box::<[i32]>::try_new_uninit_slice(1).expect("alloc"); - assert!(slot.len() == 1); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot = Box::<[i32]>::try_new_uninit_slice(len).expect("alloc"); + assert!(slot.len() == len); assert!(Box::<[u64]>::try_new_uninit_slice(usize::MAX).is_err()); } #[kani::proof] + #[kani::unwind(4)] pub fn check_try_new_zeroed_slice() { - let slot = Box::<[u8]>::try_new_zeroed_slice(1).expect("alloc"); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot = Box::<[u8]>::try_new_zeroed_slice(len).expect("alloc"); let boxed = unsafe { slot.assume_init() }; - assert!(boxed[0] == 0); + assert!(boxed.len() == len); + for i in 0..len { + assert!(boxed[i] == 0); + } assert!(Box::<[u64]>::try_new_zeroed_slice(usize::MAX).is_err()); } @@ -2573,28 +2618,39 @@ mod verify { } #[kani::proof] + #[kani::unwind(4)] pub fn check_new_uninit_slice_in() { - let slot: Box<[MaybeUninit], _> = Box::new_uninit_slice_in(1, Global); - assert!(slot.len() == 1); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot: Box<[MaybeUninit], _> = Box::new_uninit_slice_in(len, Global); + assert!(slot.len() == len); } #[kani::proof] + #[kani::unwind(4)] pub fn check_new_zeroed_slice_in() { - let slot: Box<[MaybeUninit], _> = Box::new_zeroed_slice_in(1, Global); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot: Box<[MaybeUninit], _> = Box::new_zeroed_slice_in(len, Global); let boxed = unsafe { slot.assume_init() }; - assert!(boxed[0] == 0); + assert!(boxed.len() == len); + for i in 0..len { + assert!(boxed[i] == 0); + } } #[kani::proof] + #[kani::unwind(4)] pub fn check_try_new_uninit_slice_in() { - let slot = Box::<[i32]>::try_new_uninit_slice_in(0, Global).expect("zst/empty"); - assert!(slot.is_empty()); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot = Box::<[i32]>::try_new_uninit_slice_in(len, Global).expect("alloc"); + assert!(slot.len() == len); } #[kani::proof] + #[kani::unwind(4)] pub fn check_try_new_zeroed_slice_in() { - let slot = Box::<[u8]>::try_new_zeroed_slice_in(1, Global).expect("alloc"); - assert!(slot.len() == 1); + let len = kani::any_where(|n: &usize| *n <= SLICE_CAP); + let slot = Box::<[u8]>::try_new_zeroed_slice_in(len, Global).expect("alloc"); + assert!(slot.len() == len); } #[kani::proof] From 4da62f00d5c02a9d1ba4457da136be459a539212 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Sat, 22 Aug 2026 13:09:40 +0530 Subject: [PATCH 5/5] fix: allocate slice without Box::from in from_raw_in harness proof_for_contract allows one top-level from_raw_in call. Box::from already goes through from_raw_in, so macos partition 2 failed check_from_raw_in_slice. Mirror alloc_write for [u8]. --- library/alloc/src/boxed.rs | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs index 81aefd521f3a6..4ecd20525662a 100644 --- a/library/alloc/src/boxed.rs +++ b/library/alloc/src/boxed.rs @@ -2361,6 +2361,21 @@ mod verify { } } + /// Heap-allocate a `[u8]` without `Box::from` / `from_raw_in` (Kani + /// `proof_for_contract` allows only one top-level call to the contracted fn). + fn alloc_write_slice(data: &[u8]) -> *mut [u8] { + let len = data.len(); + let ptr = if len == 0 { + NonNull::::dangling().as_ptr() + } else { + let layout = Layout::array::(len).expect("layout"); + let ptr = Global.allocate(layout).expect("alloc").cast::().as_ptr(); + unsafe { ptr::copy_nonoverlapping(data.as_ptr(), ptr, len) }; + ptr + }; + ptr::slice_from_raw_parts_mut(ptr, len) + } + // ---- required unsafe: assume_init (sized) ---- #[kani::proof_for_contract(Box::, A>::assume_init)] @@ -2490,10 +2505,9 @@ mod verify { pub fn check_from_raw_in_slice() { let data: [u8; SLICE_CAP] = kani::any(); let slice = kani::slice::any_slice_of_array(&data); - let boxed: Box<[u8]> = Box::from(slice); - let len = boxed.len(); - let (ptr, alloc) = Box::into_raw_with_allocator(boxed); - let boxed = unsafe { Box::from_raw_in(ptr, alloc) }; + let len = slice.len(); + let ptr = alloc_write_slice(slice); + let boxed = unsafe { Box::from_raw_in(ptr, Global) }; assert!(boxed.len() == len); } @@ -2517,10 +2531,9 @@ mod verify { pub fn check_from_non_null_in_slice() { let data: [u8; SLICE_CAP] = kani::any(); let slice = kani::slice::any_slice_of_array(&data); - let boxed: Box<[u8]> = Box::from(slice); - let len = boxed.len(); - let (ptr, alloc) = Box::into_non_null_with_allocator(boxed); - let boxed = unsafe { Box::from_non_null_in(ptr, alloc) }; + let len = slice.len(); + let ptr = NonNull::new(alloc_write_slice(slice)).unwrap(); + let boxed = unsafe { Box::from_non_null_in(ptr, Global) }; assert!(boxed.len() == len); }