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

[sankalpsthakur]

Summary

Kani safety contracts and proof harnesses for Challenge 29 (Box / convert / ThinBox). Runtime stdlib logic is unchanged; annotations are cfg(kani) plus the repo-standard tool-agnostic safety::{requires, ensures} attributes (not cfg_attr(kani, kani::requires)).

In-window ticket (end 2026-12-31, $15,000 USD). Tracking #526.

Success criteria mapping

Required unsafe functions (contracts + verified harnesses):

• Box<MaybeUninit<T>, A>::assume_init and slice form — #[requires]/#[ensures] + proof_for_contract
• Box::from_raw, from_non_null, from_raw_in, from_non_null_in — same, including sized + slice instantiations. Reconstructors require a layout predicate: ub_checks::can_dereference and Layout::for_value_raw size <= isize::MAX (allocator provenance is a caller obligation we cannot express). Slice from_raw_in / from_non_null_in harnesses allocate without Box::from so proof_for_contract sees a single top-level call.
• Unchecked downcast: the challenge table lists <dyn Error>::downcast_unchecked (×3). That API does not exist in this tree (impl dyn Error only has safe downcast). The three real methods are Box<dyn Any (+ Send) (+ Sync), A>::downcast_unchecked. Those three carry safety contracts; harnesses execute the bodies under is::<T>(). Kani cannot proof_for_contract the trait-object generic methods (resolver lists the three impls and rejects angle-bracket paths).

Safe wrappers (≥75% of 46): 45/46 covered (the listed TryFrom<Box<T>> impl does not exist; TryFrom<Vec<T>> is extra). Includes ThinBox Deref/DerefMut/Drop/meta/with_header and WithHeader::{new, try_new, new_unsize_zst, header}, from_slice (TrivialClone + Clone), Error/Any downcast ok/err paths, into_pin with !Unpin. Slice constructors and reconstructors use bounded symbolic lengths (kani::any_where / any_slice_of_array), not only fixed 0/1.

UBs: dangling/misaligned access, intrinsic UB, mutating immutable bytes, invalid values — via Kani's default checks on the real std bodies. No cfg(not(kani)) body swap.

Validation

• Worktree challenge/29-boxed, head 4da62f00d5c02a9d1ba4457da136be459a539212
• Authoritative launch is GitHub Actions scripts/run-kani.sh
• Kani run 32560286046: partitions 1–4 SUCCESS on ubuntu and macos. Autoharness ubuntu Complete - 1447 successfully verified harnesses, 0 failures. Autoharness macos Complete - 1446 successfully verified harnesses, 0 failures. Kani List, Metrics, Autoharness Analyzer, Build JSON SUCCESS.
• Flux, GOTO, VeriFast, KMIR, upstream_test ubuntu+macos, simd, build: SUCCESS

Fixes #526

AI/LLM disclosure

• AI coding tools (including Grok and/or Codex agent-assisted editing) were used to help draft or modify code and this PR description.
• I reviewed the complete change, understand the reasoning, and take responsibility for the contracts and harnesses.
• This submission is original work of authorship under the project contributor terms; AI output was not pasted unreviewed.

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