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
• 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) — same limitation as other Challenge 29 submissions.

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.

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 5d8f0ee99218643bc7eb62fe39aa70b6c43508cb
• Authoritative launch is GitHub Actions scripts/run-kani.sh
• On this SHA: Kani partitions 1–4 SUCCESS (ubuntu; ~27–43 min). Autoharness macos SUCCESS: Complete - 1444 successfully verified harnesses, 0 failures (job 96454587856, 56 min). Ubuntu autoharness SUCCESS: Complete - 1445 successfully verified harnesses, 0 failures (job 96454587592, 1h12m). Prior SHA b389760 had 3 convert CBMC timeouts; slim on this SHA cleared them on both OS..
• upstream_test ubuntu+macos, Flux, GOTO, VeriFast, simd models, build: SUCCESS
• Local kani 0.67.0 on the three previously-timing harnesses: VERIFICATION SUCCESSFUL <0.5s each

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.