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).

[v3risec]

Thanks for the thoughtful review. We have addressed the review comments about grouping Kani harnesses.

Changes made:

• Consolidated the numbered verify_* modules into a single mod verify in:
  • library/alloc/src/boxed.rs
  • library/alloc/src/boxed/convert.rs
  • library/alloc/src/boxed/thin.rs
• Kept the existing harness bodies unchanged.
• Moved repeated imports to the consolidated module scope.

One note on the import-path review comment in convert.rs: we kept
super::super::kani_box_harness_helpers::*. These imports are now inside
crate::boxed::convert::verify, so super resolves to crate::boxed::convert
and super::super resolves to crate::boxed, where
kani_box_harness_helpers is defined. Using super::kani_box_harness_helpers::*
does not compile.

[feliperodri]

Challenge 29 (Boxed) — Kani verification review of PR #589

Verdict: sound, no fatal issues; a few non-blocking concerns

This is a large, carefully-structured submission (macro-generated harnesses over primitive instantiations, per the challenge's "primitive types only" allowance). I could not find any soundness-breaking pattern.

Soundness checklist

1. cfg-swap vacuity (FATAL): none. All contracts are added via #[cfg_attr(kani, kani::requires(...))] / kani::ensures(...); no #[cfg(not(kani))] body substitution exists. No trivially-passing harnesses.
2. Assume documented precondition vs. assume-the-conclusion: legitimate. For downcast_unchecked the harnesses do kani::assume(erased.is::<$ty>()) (convert.rs ~2159/2201/2247) — this restates the documented precondition, and since erased genuinely holds $ty the assume is always satisfiable (not over-constrained, not conclusion-assuming).
3. Genuinely symbolic inputs. verifier_nondet_vec (boxed.rs 299-315) builds symbolic-length, symbolic-byte vectors; slice harnesses use kani::any_where(|l| box_slice_layout_ok::<T>(*l)) keeping length unbounded/symbolic. into_array/try_from fix N=100 but keep vec.len() symbolic, so both the len==N and len!=N branches are explored (boxed.rs 1042-1058, convert.rs 2351-2367). Not concrete-only unit tests.
4. Faithful, truly-verified contracts on the raw-pointer reconstruction fns. from_raw, from_non_null, from_raw_in, from_non_null_in get requires(!null && checked_align_of_raw.is_some() && size <= isize::MAX && can_dereference) plus ensures((&**result) as *const T == raw) (boxed.rs 204-283), and are verified with #[kani::proof_for_contract(...)] across sized + unsized (slice) instantiations. These preconditions are the actual documented safety requirements — non-trivial and meaningful.

Success-criteria coverage

• The 9 required unsafe fns are all addressed. assume_init (sized + slice), from_raw, from_non_null, from_raw_in, from_non_null_in, and the three downcast_unchecked.
• Targeting is correct — the challenge doc table is stale. The table lists <dyn Error>::downcast_unchecked, but I verified (grep -rn "fn downcast_unchecked" library/) that no such function exists: in alloc::boxed::convert the only downcast_unchecked methods are the three on Box<dyn Any, A> (convert.rs 394/453/512), and impl dyn Error (convert.rs 736-779) exposes only the safe downcast. PR #589 added contracts + harnesses to exactly those three real Box<dyn Any>::downcast_unchecked functions — this is the right target, contrary to the task note's premise. It additionally verifies the safe <dyn Error>::downcast family (ok/err paths, convert.rs 2617-2757).
• ThinBox/WithHeader family fully covered in thin.rs: Deref, DerefMut, Drop, meta, with_header, WithHeader::{new, try_new, new_unsize_zst, header} across sized/dyn Any/slice instantiations. (This is exactly what the competing #573 lacked.)
• Safe-fn coverage is well above the 75% bar — essentially every entry in the safe table has harness(es), including Drop, Default, Clone, into_pin (with a !Unpin sentinel), leak, into_unique, all the *_slice_in/try_new_* constructors, and the convert From/TryFrom paths.

Non-blocking issues (worth addressing before merge)

1. Contract style deviates from the repo convention (upstreamability). The repo uses the tool-agnostic safety crate everywhere: grep -rln "use safety::" library/core/src library/alloc/src = 46 files, while cfg_attr(kani, kani::requires = 0. This PR hardcodes #[cfg_attr(kani, kani::requires/ensures(...))] (e.g. boxed.rs 176-215, convert.rs 2044/2052/2060). It works under Kani (run-kani passes -Z function-contracts), so verification validity is unaffected, but maintainers will likely want use safety::{requires, ensures}; for consistency and upstreamability (a stated review criterion).
2. 5 of the 9 unsafe fns' contracts are not verified via proof_for_contract. assume_init (×2) and downcast_unchecked (×3) carry contracts but are exercised with plain #[kani::proof] that restate the precondition via kani::assume/by construction (documented as Kani limitations: MaybeUninit generic impl, and trait-object generic method target resolution — boxed.rs 358-365, convert.rs 2140-2147). The concrete safety (UB-freedom of the real body) is verified, but the contract text is not machine-linked to the proof, so it could drift without a proof failing. The 4 pointer-reconstruction fns are the ones with true proof_for_contract linkage. Consider noting this gap explicitly, or filing/​referencing the Kani limitation issues.
3. Minor coverage gap: I did not find a dedicated harness for <Box<[T]> as BoxFromSlice<T>>::from_slice from the safe table. Coverage remains far above 75%, so non-blocking.

Copilot review notes — mostly reject/stale

• Copilot's two comments that super::super::kani_box_harness_helpers "won't compile / resolves to alloc::…" are incorrect. convert/thin are declared mod convert;/mod thin; inside boxed.rs (boxed.rs 212/216), so from alloc::boxed::convert::verify, super::super = alloc::boxed, and the path correctly reaches alloc::boxed::kani_box_harness_helpers. Its suggested fix (super::kani_box_harness_helpers) would point at a non-existent alloc::boxed::convert::kani_box_harness_helpers and break the build. Do not apply.
• Copilot's "consolidate the many numbered verify_170/verify_944 modules" comments are stale — no mod verify_NNN exists in the current diff (grep -rn "mod verify_[0-9]" library/ = empty); the PR already uses a single #[cfg(kani)] mod verify per file, matching the repo convention it cites.

Bottom line

Sound, vacuity-free, correctly-targeted, and exceeds the coverage bar, with the ThinBox/WithHeader family that the competing PR lacked. Recommend COMMENT: address the safety-crate contract style and clarify the non-proof_for_contract subset before approval; no changes are required for verification soundness.