Challenge 29: Kani contracts for Box, convert, and ThinBox

[sankalpsthakur]

Fixes #526 (Challenge 29: Box, convert and ThinBox).

Add safety contracts and Kani harnesses using the repository's safety::{requires, ensures} annotations. Runtime stdlib logic is unchanged.

Coverage includes assume-init methods, raw/non-null reconstructors, ThinBox operations, slice constructors, downcast paths and pinning. Slice harnesses use bounded symbolic lengths. Reconstructor contracts check dereferenceability and layout bounds; allocator provenance remains a caller obligation that these contracts cannot express.

The challenge's unchecked dyn Error methods do not exist in this tree. The actual Box<dyn Any> variants receive contracts and body-executing harnesses, but Kani's trait-object resolver prevents proof_for_contract on them. The listed TryFrom<Box<T>> implementation also does not exist; TryFrom<Vec<T>> is covered separately.

Validation

At 4da62f00d5c02a9d1ba4457da136be459a539212, GitHub Actions run 32560286046 passed Kani partitions 1 through 4 on Ubuntu and macOS. Autoharness reported 1,447 verified harnesses on Ubuntu and 1,446 on macOS, with zero failures. The listed Kani analysis, Flux, GOTO, VeriFast, KMIR, upstream, SIMD and build checks also succeeded. These are run-level results, not counts of new harnesses in this PR.

AI coding tools assisted with the contracts, harnesses and this description.

[sankalpsthakur]

Ready for committee FCFS review of Challenge 29 (in-window, end 2026-12-31).

Head 5d8f0ee99218643bc7eb62fe39aa70b6c43508cb:

• Kani partitions 1–4 SUCCESS
• Autoharness ubuntu: 1445 harnesses, 0 failures
• Autoharness macos: 1444 harnesses, 0 failures
• Flux, GOTO, VeriFast, upstream_test SUCCESS
• Contracts use repo-standard safety::{requires, ensures}

Tracking Fixes #526. No second solution PR.

[feliperodri]

Approving — leading solution for Challenge 29

Thanks @sankalpsthakur. After reviewing all three open Challenge 29 (boxed) solutions with our vacuity tooling and local Kani (pinned 0.67.0 / CBMC 6.8.0), this is complete, sound, and the most concise. Prioritizing it.

Coverage against Ch29 criteria:

• A: 9/9 unsafe fns with contracts + verified. assume_init (sized+slice), from_raw, from_non_null, from_raw_in, from_non_null_in are verified via #[kani::proof_for_contract] (6). The 3 downcast_unchecked methods carry contracts and are exercised via plain #[kani::proof] with the precondition mirrored by kani::assume — Kani cannot resolve proof_for_contract on a trait-object generic method (Box<dyn Any>::downcast_unchecked::<T>), the documented/accepted workaround. Note the 3 challenge-listed <dyn Error>::downcast_unchecked don't exist in std — the real methods are Box<dyn Any(+Send)(+Sync)>::downcast_unchecked, which you correctly verified (disclosed in the PR).
• B: 45/46 safe abstractions (97.8%, ≥ 75%). Only <Box<[T;N]> as TryFrom<Box<T>>>::try_from (which doesn't exist in-tree) is uncovered.

Soundness (all clean):

• T1: no cfg body swaps — 906 lines pure additions, no - lines; the only cfg-gated code is the box_ptr_fits_box_layout helper used in requires clauses.
• T2: no trivial invariants, no loop_invariant(true); slice iteration uses unwind(4) for len ≤ 2 (non-vacuous).
• T7: 6/9 unsafe fns + boxed_slice_as_array_unchecked have proof_for_contract; the 3 downcast_unchecked + WithHeader::drop are assume-mirror (Kani trait-object limitation, disclosed). Autoharness allowlist unchanged.
• Not assume-the-conclusion — downcast harnesses build Box::new(concrete) then downcast to the same type; the is::<T>() witness is real, not assumed.
• Inputs symbolic (kani::any()); primitive-mono is challenge-allowed; no unbounded clause. No runtime std logic changed.

Local Kani sample (CBMC 6.8.0): 4/4 VERIFICATION SUCCESSFUL — check_assume_init_i32 (proof_for_contract), check_from_raw_i32 (proof_for_contract), check_downcast_unchecked_any, check_leak.

Minor note (non-blocking): the 3 Box<dyn Any>::downcast_unchecked contracts and WithHeader::drop rely on assume-mirror rather than proof_for_contract (Kani limitation) — worth a tracking note so they can be upgraded if kani gains trait-object contract resolution. Complete and sound as-is.