Challenge 29: Verify Boxed safety in alloc::boxed, alloc::boxed::convert and alloc::boxed::thin with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Box, ThinBox, and related boxed conversion APIs in library/alloc/src/boxed.rs, library/alloc/src/boxed/convert.rs, and library/alloc/src/boxed/thin.rs for Challenge 29.

The change introduces:

• proof harness modules under #[cfg(kani)] for the required unsafe functions and a broad safe-function subset
• contracts for unsafe boxed pointer reconstruction, initialization, and unchecked downcast APIs
• reusable helper macros and harness setup for representative concrete instantiations, including sized values, slices, arrays, strings, trait objects, and allocator-aware APIs

No non-verification runtime behavior is changed in normal builds.

Notes on Challenge 29 Function Signatures

Several Challenge 29 entries do not exactly match the current repository source. This PR follows the actual checked-in API signatures rather than the likely stale or imprecise challenge text.

Notable mismatches include:

• The slice allocation APIs are listed as Box<T, A>::new_uninit_slice_in, Box<T, A>::new_zeroed_slice_in, Box<T, A>::try_new_uninit_slice_in, and Box<T, A>::try_new_zeroed_slice_in, but the current source implements them on Box<[T], A> and returns boxed [MaybeUninit<T>] slices.
• The challenge entry <Box<[T; N]> as TryFrom<Box<T>>>::try_from does not match the source. The current implementation is <Box<[T; N]> as TryFrom<Vec<T>>>::try_from.
• The required unchecked downcast entries are written as <dyn Error>::downcast_unchecked variants in the challenge text, but the current source provides unchecked downcast APIs for Box<dyn Any, A>, Box<dyn Any + Send, A>, and Box<dyn Any + Send + Sync, A>.
• Several entries omit important bounds such as T: ?Sized, T: Clone, allocator bounds, or specialization-related constraints. The harnesses use the bounds from the actual source definitions.

Verification Coverage Report

Unsafe functions

Coverage: 9 / 9 (100%)

Verified set includes:

• Box<mem::MaybeUninit<T>, A>::assume_init
• Box<[mem::MaybeUninit<T>], A>::assume_init
• Box<T>::from_raw
• Box<T>::from_non_null
• Box<T, A>::from_raw_in
• Box<T, A>::from_non_null_in
• Box<dyn Any, A>::downcast_unchecked
• Box<dyn Any + Send, A>::downcast_unchecked
• Box<dyn Any + Send + Sync, A>::downcast_unchecked

Safe functions

Coverage: 45 / 46 (97.8%)

This exceeds the Challenge 29 threshold of at least 75%.

Covered safe functions include APIs from the following groups:

Allocation and initialization

• Box<[T], A>::new_uninit_slice_in
• Box<[T], A>::new_zeroed_slice_in
• Box<[T], A>::try_new_uninit_slice_in
• Box<[T], A>::try_new_zeroed_slice_in
• Box<mem::MaybeUninit<T>, A>::write

Raw pointer and ownership conversion

• Box<T>::into_non_null
• Box<T, A>::into_raw_with_allocator
• Box<T, A>::into_non_null_with_allocator
• Box<T, A>::into_unique
• Box<T, A>::leak
• Box<T, A>::into_pin

Trait implementations for Box

• <Box<T, A> as Drop>::drop
• <Box<T> as Default>::default
• <Box<str> as Default>::default
• <Box<T, A> as Clone>::clone
• <Box<str> as Clone>::clone
• <Box<str> as From<&str>>::from
• <Box<[u8], A> as From<Box<str, A>>>::from
• <Box<[T; N]> as TryFrom<Box<[T]>>>::try_from
• <Box<[T; N]> as TryFrom<Vec<T>>>::try_from

Box<dyn Any> and Box<dyn Error> conversions

• Box<dyn Any, A>::downcast
• Box<dyn Any + Send, A>::downcast
• Box<dyn Any + Send + Sync, A>::downcast
• <dyn Error>::downcast
• <dyn Error + Send>::downcast
• <dyn Error + Send + Sync>::downcast

ThinBox and WithHeader

• <ThinBox<T> as Deref>::deref
• <ThinBox<T> as DerefMut>::deref_mut
• <ThinBox<T> as Drop>::drop
• ThinBox<T>::meta
• ThinBox<T>::with_header
• WithHeader<H>::new
• WithHeader<H>::try_new
• WithHeader<H>::new_unsize_zst
• WithHeader<H>::header

Not listed as a standalone harness target:

• <Box<[T]> as BoxFromSlice<T>>::from_slice

Approach

The verification strategy combines contracts for unsafe entry points with executable proof harnesses:

1. Unsafe function contracts

• Add kani::requires preconditions for pointer non-nullness, layout compatibility, dereferenceability, and initialization where expressible.
• Attach proof harnesses with #[kani::proof_for_contract] for the required unsafe APIs.

2. Harness-backed behavioral checks

• Add dedicated #[kani::proof] harnesses for safe APIs across allocation, conversion, trait implementation, downcast, ThinBox, and WithHeader behavior.

3. Representative instantiations

• Instantiate generic APIs with representative concrete types, including integer types, bool, unit, arrays, slices, strings, dyn Any, dyn Error, and allocator-aware Global cases.

4. Challenge alignment

• Keep all verification code under cfg(kani) so normal std behavior is unchanged.
• Target Challenge 29’s success criteria directly: full required unsafe coverage and safe-function coverage well above the required threshold.

Scope assumptions

• Generic T is instantiated with representative concrete types allowed by the challenge.
• Allocator-focused proofs are limited to standard-library allocator scope, primarily Global.
• Some properties such as exact allocator provenance and unique ownership for raw pointer reconstruction are partially constrained by the predicates currently available to Kani; harnesses use the strongest practical source-aligned preconditions available in this codebase.

Verification

All added Challenge 29 harnesses pass locally with Kani.

Resolves #526

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Adds Kani-based verification artifacts for Challenge 29 across alloc::boxed (including ThinBox) by introducing Kani harness modules and attaching Kani-only contracts (cfg_attr(kani, ...)) to selected unsafe APIs, without altering normal runtime behavior.

Changes:

• Adds Kani preconditions/postconditions to boxed raw-pointer reconstruction and unchecked downcast APIs.
• Introduces extensive #[cfg(kani)] proof harness modules for Box, ThinBox, and header utilities across representative concrete instantiations.
• Updates library/Cargo.lock to include the safety proc-macro crate (and its transitive deps) in the lockfile dependency graph.

Reviewed changes

Copilot reviewed 3 out of 4 changed files in this pull request and generated 5 comments.

File	Description
library/alloc/src/boxed.rs	Adds Kani-only contracts for unsafe Box APIs and a large set of Kani proof harnesses/helpers for Challenge 29 coverage.
library/alloc/src/boxed/convert.rs	Adds Kani-only preconditions to downcast_unchecked variants and adds harnesses for boxed conversions/downcasts.
library/alloc/src/boxed/thin.rs	Adds Kani proof harnesses for ThinBox deref/drop/meta/header-related behavior.
library/Cargo.lock	Lockfile updates to reflect safety crate usage and its proc-macro dependencies.

[Copilot]

kani_box_harness_helpers is defined as a sibling module of convert under alloc::boxed (in boxed.rs), so super::super::kani_box_harness_helpers resolves to alloc::kani_box_harness_helpers and won’t compile. Use super::kani_box_harness_helpers (or crate::boxed::kani_box_harness_helpers) instead so the harness can see verifier_nondet_vec_box.

Suggested change

	use super::super::kani_box_harness_helpers::*;
	use super::kani_box_harness_helpers::*;

[Copilot]

Same issue here: super::super::kani_box_harness_helpers points at the alloc module, not the boxed module where kani_box_harness_helpers is declared. This will fail to compile under cfg(kani); refer to the helper module via super::kani_box_harness_helpers (or crate::boxed::kani_box_harness_helpers).

Suggested change

	use super::super::kani_box_harness_helpers::*;
	use super::kani_box_harness_helpers::*;

[Copilot]

The repository’s existing Kani harnesses are typically grouped under a single #[cfg(kani)] ... mod verify { ... } block (e.g. library/alloc/src/vec/mod.rs:4307-4353, library/alloc/src/collections/vec_deque/mod.rs:3274-3312). Using many numbered modules like verify_170, verify_251, etc. makes the verification surface harder to navigate and is inconsistent with that convention; consider consolidating into one mod verify (with submodules if needed).

[Copilot]

The repository’s existing Kani harnesses are typically grouped under a single #[cfg(kani)] ... mod verify { ... } block (e.g. library/alloc/src/vec/mod.rs:4307-4353, library/alloc/src/collections/vec_deque/mod.rs:3274-3312). This file introduces multiple numbered modules like verify_146, verify_156, etc., which is inconsistent with that convention and makes it harder to find harnesses; consider consolidating into one mod verify (submodules/macros inside as needed).

Suggested change

	mod verify_146 {
	mod verify {

[Copilot]

The repository’s existing Kani harnesses are typically grouped under a single #[cfg(kani)] ... mod verify { ... } block (e.g. library/alloc/src/vec/mod.rs:4307-4353, library/alloc/src/collections/vec_deque/mod.rs:3274-3312, and many library/core/src/** files). Adding dozens of separate numbered modules (verify_944, verify_1011, …) is inconsistent with that convention and makes the verification code harder to maintain; consider consolidating under one mod verify (with internal submodules for organization).